ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>AdicCompletion.eval I M n ∘ₗ AdicCompletion.of I M = (I ^ n • ⊤).mkQ
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>Function.Surjective ⇑(AdicCompletion.eval I M n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>LinearMap.range (AdicCompletion.eval I M n) = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>↑0 n = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>f g : AdicCompletion I M<GOAL>↑(f + g) n = ↑f n + ↑g n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>f g : AdicCompletion I M<GOAL>↑(f - g) n = ↑f n - ↑g n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>α : Type u_4<VAR>s : Finset α<VAR>f : α → AdicCompletion I M<VAR>n : ℕ<GOAL>↑(s.sum f) n = ∑ a ∈ s, ↑(f a) n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>r : R<VAR>f : AdicCompletion I M<GOAL>↑(r • f) n = r • ↑f n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : AdicCompletion I M<VAR>h : ∀ (n : ℕ), ↑x n = ↑y n<GOAL>x = y
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : AdicCompletion I M<GOAL>x = y ↔ ∀ (n : ℕ), ↑x n = ↑y n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>x : M<GOAL>(AdicCompletion.transitionMap I M hmn) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<GOAL>AdicCompletion.transitionMap I M ⋯ = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>AdicCompletion.transitionMap I M hmn ∘ₗ AdicCompletion.transitionMap I M hnk = AdicCompletion.transitionMap I M ⋯
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<VAR>x : M ⧸ I ^ k • ⊤<GOAL>(AdicCompletion.transitionMap I M hmn) ((AdicCompletion.transitionMap I M hnk) x) = (AdicCompletion.transitionMap I M ⋯) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>x : AdicCompletion I M<GOAL>(AdicCompletion.transitionMap I M hmn) (↑x n) = ↑x m
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>AdicCompletion.transitionMap I M hmn ∘ₗ AdicCompletion.eval I M n = AdicCompletion.eval I M m
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>f g : AdicCompletion.AdicCauchySequence I M<GOAL>↑(f + g) n = ↑f n + ↑g n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>f g : AdicCompletion.AdicCauchySequence I M<GOAL>↑(f - g) n = ↑f n - ↑g n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>n : ℕ<VAR>r : R<VAR>f : AdicCompletion.AdicCauchySequence I M<GOAL>↑(r • f) n = r • ↑f n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : AdicCompletion.AdicCauchySequence I M<VAR>h : ∀ (n : ℕ), ↑x n = ↑y n<GOAL>x = y
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : AdicCompletion.AdicCauchySequence I M<GOAL>x = y ↔ ∀ (n : ℕ), ↑x n = ↑y n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>f : AdicCompletion.AdicCauchySequence I M<GOAL>Submodule.Quotient.mk (↑f n) = Submodule.Quotient.mk (↑f m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f : ℕ → M<GOAL>AdicCompletion.IsAdicCauchy I M f ↔ ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f : ℕ → M<VAR>h : ∀ (n : ℕ), f n ≡ f (n + 1) [SMOD I ^ n • ⊤]<GOAL>∀ (a : ℕ), ↑(AdicCompletion.AdicCauchySequence.mk I M f h) a = f a
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f : AdicCompletion.AdicCauchySequence I M<VAR>n : ℕ<GOAL>↑((AdicCompletion.mk I M) f) n = (I ^ n • ⊤).mkQ (↑f n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>f : AdicCompletion.AdicCauchySequence I M<VAR>h : ∃ k, ∀ n ≥ k, ∃ m ≥ n, ∃ l ≥ n, ↑f m ∈ I ^ l • ⊤<GOAL>(AdicCompletion.mk I M) f = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>Function.Surjective ⇑(AdicCompletion.mk I M)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>p : AdicCompletion I M → Prop<VAR>x : AdicCompletion I M<VAR>h : ∀ (f : AdicCompletion.AdicCauchySequence I M), p ((AdicCompletion.mk I M) f)<GOAL>p x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤<VAR>h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m<VAR>n : ℕ<GOAL>AdicCompletion.eval I N n ∘ₗ AdicCompletion.lift I f ⋯ = f n
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤<VAR>h : ∀ {m n : ℕ} (hle : m ≤ n), AdicCompletion.transitionMap I N hle ∘ₗ f n = f m<VAR>n : ℕ<VAR>x : M<GOAL>↑((AdicCompletion.lift I f ⋯) x) n = (f n) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>h : IsAdicComplete ⊤ M<GOAL>Subsingleton M
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>IsAdicComplete I R<GOAL>I ≤ ⊥.jacobson
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : Polynomial R<GOAL>p.IsPrimitive ↔ ∀ (r : R), Polynomial.C r ∣ p → IsUnit r
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>Polynomial.IsPrimitive 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p : Polynomial R<VAR>hp : p.Monic<GOAL>p.IsPrimitive
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>p : Polynomial R<VAR>hp : p.IsPrimitive<GOAL>p ≠ 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>p q : Polynomial R<VAR>hp : p.IsPrimitive<VAR>hq : q ∣ p<GOAL>q.IsPrimitive
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<VAR>n : ℕ<GOAL>p.content ∣ p.coeff n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>r : R<GOAL>(Polynomial.C r).content = normalize r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<GOAL>Polynomial.content 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<GOAL>Polynomial.content 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>(Polynomial.X * p).content = p.content
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>k : ℕ<GOAL>(Polynomial.X ^ k).content = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<GOAL>Polynomial.X.content = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>r : R<VAR>p : Polynomial R<GOAL>(Polynomial.C r * p).content = normalize r * p.content
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>r : R<VAR>k : ℕ<GOAL>((Polynomial.monomial k) r).content = normalize r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.content = 0 ↔ p = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>normalize p.content = p.content
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>normUnit p.content = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<VAR>n : ℕ<VAR>h : p.natDegree < n<GOAL>p.content = (Finset.range n).gcd p.coeff
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.content = (Finset.range p.natDegree.succ).gcd p.coeff
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.content = gcd p.leadingCoeff p.eraseLead.content
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<VAR>r : R<GOAL>r ∣ p.content ↔ Polynomial.C r ∣ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>Polynomial.C p.content ∣ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.IsPrimitive ↔ p.content = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<VAR>hp : p.IsPrimitive<GOAL>p.content = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p = Polynomial.C p.content * p.primPart
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<GOAL>Polynomial.primPart 0 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.primPart.IsPrimitive
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.primPart.content = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.primPart ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.primPart.natDegree = p.natDegree
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<VAR>hp : p.IsPrimitive<GOAL>p.primPart = p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>r : R<GOAL>IsUnit (Polynomial.C r).primPart
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<GOAL>p.primPart ∣ p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>Ring S<VAR>IsDomain S<VAR>Algebra R S<VAR>NoZeroSMulDivisors R S<VAR>p : Polynomial R<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : (Polynomial.aeval s) p = 0<GOAL>(Polynomial.aeval s) p.primPart = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>IsDomain S<VAR>f : R →+* S<VAR>hinj : Function.Injective ⇑f<VAR>p : Polynomial R<VAR>s : S<VAR>hpzero : p ≠ 0<VAR>hp : Polynomial.eval₂ f s p = 0<GOAL>Polynomial.eval₂ f s p.primPart = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>a : R<VAR>p q : Polynomial R<VAR>h : Polynomial.C a ∣ p - q<GOAL>gcd a p.content = gcd a q.content
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : Polynomial R<GOAL>gcd (p * q).eraseLead.content p.leadingCoeff = gcd (p.eraseLead * q).content p.leadingCoeff
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : Polynomial R<GOAL>(p * q).content = p.content * q.content
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : Polynomial R<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<GOAL>(p * q).IsPrimitive
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : Polynomial R<VAR>h0 : p * q ≠ 0<GOAL>(p * q).primPart = p.primPart * q.primPart
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : Polynomial R<VAR>hp : p.IsPrimitive<VAR>hq : q ≠ 0<GOAL>p ∣ q.primPart ↔ p ∣ q
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : Polynomial R<VAR>hp : p.IsPrimitive<VAR>hq : q.IsPrimitive<GOAL>∃ r, r.IsPrimitive ∧ ∀ (s : Polynomial R), p ∣ s ∧ q ∣ s ↔ r ∣ s
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p q : Polynomial R<VAR>hq : q ≠ 0<GOAL>p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<VAR>hp : p ≠ 0<VAR>q : Polynomial R<GOAL>(gcd p q).degree ≤ p.degree
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>NormalizedGCDMonoid R<VAR>p : Polynomial R<VAR>q : Polynomial R<VAR>hq : q ≠ 0<GOAL>(gcd p q).degree ≤ q.degree
<GOAL>RingHom.StableUnderComposition fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
<GOAL>RingHom.RespectsIso fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
<GOAL>RingHom.StableUnderBaseChange fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
<GOAL>RingHom.OfLocalizationSpan fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∈ Module.support R M ↔ Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∉ Module.support R M ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∉ Module.support R M ↔ ∀ (m : M), ∃ r ∉ p.asIdeal, r • m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∈ Module.support R M ↔ ∃ m, ∀ r ∉ p.asIdeal, r • m ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<GOAL>p ∈ Module.support R M ↔ ∃ m, (Submodule.span R {m}).annihilator ≤ p.asIdeal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<VAR>s : Set M<VAR>hs : Submodule.span R s = ⊤<GOAL>p ∈ Module.support R M ↔ ∃ m ∈ s, (Submodule.span R {m}).annihilator ≤ p.asIdeal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<VAR>hp : p ∈ Module.support R M<GOAL>Module.annihilator R M ≤ p.asIdeal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : R<GOAL>Subsingleton (LocalizedModule (Submonoid.powers f) M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.support R M = ∅ ↔ Subsingleton M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Subsingleton M<GOAL>Module.support R M = ∅
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_3<VAR>Ring A<VAR>Algebra R A<GOAL>Module.support R A = PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>Nontrivial M<GOAL>Module.support R M = Set.univ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>p : PrimeSpectrum R<VAR>Module.Finite R M<GOAL>p ∈ Module.support R M ↔ Module.annihilator R M ≤ p.asIdeal
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<GOAL>Module.support R M ⊆ Module.support R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<GOAL>Module.support R N ⊆ Module.support R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : Function.Exact ⇑f ⇑g<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>Module.support R N = Module.support R M ∪ Module.support R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>e : M ≃ₗ[R] N<GOAL>Module.support R M = Module.support R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<GOAL>Module.support R M = PrimeSpectrum.zeroLocus ↑(Module.annihilator R M)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>p : Ideal R<VAR>p.IsPrime<VAR>Subsingleton (LocalizedModule p.primeCompl M)<GOAL>∃ f ∉ p, Subsingleton (LocalizedModule (Submonoid.powers f) M)
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>J : Ideal R<VAR>hJ : J ≤ v.supp<GOAL>Valuation.comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>J : Ideal R<VAR>v : Valuation (R ⧸ J) Γ₀<GOAL>J ≤ (Valuation.comap (Ideal.Quotient.mk J) v).supp
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>J : Ideal R<VAR>v : Valuation (R ⧸ J) Γ₀<GOAL>(Valuation.comap (Ideal.Quotient.mk J) v).onQuot ⋯ = v
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>J : Ideal R<VAR>hJ : J ≤ v.supp<GOAL>(v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>(v.onQuot ⋯).supp = 0
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>J : Ideal R<VAR>hJ : J ≤ v.supp<GOAL>AddValuation.comap (Ideal.Quotient.mk J) (v.onQuot hJ) = v
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>S : Type u_3<VAR>CommRing S<VAR>f : S →+* R<GOAL>(AddValuation.comap f v).supp = Ideal.comap f v.supp
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>J : Ideal R<VAR>v : AddValuation (R ⧸ J) Γ₀<GOAL>J ≤ (AddValuation.comap (Ideal.Quotient.mk J) v).supp
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>J : Ideal R<VAR>v : AddValuation (R ⧸ J) Γ₀<GOAL>(AddValuation.comap (Ideal.Quotient.mk J) v).onQuot ⋯ = v
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<VAR>J : Ideal R<VAR>hJ : J ≤ v.supp<GOAL>(v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp
<VAR>R : Type u_1<VAR>Γ₀ : Type u_2<VAR>CommRing R<VAR>LinearOrderedAddCommMonoidWithTop Γ₀<VAR>v : AddValuation R Γ₀<GOAL>AddValuation.supp (Valuation.onQuot v ⋯) = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>i : ι<GOAL>MeasureTheory.IsStoppingTime f fun x => i
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω ≤ i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>PredOrder ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>PartialOrder ι<VAR>τ : Ω → ι<VAR>f : MeasureTheory.Filtration ι m<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>PartialOrder ι<VAR>τ : Ω → ι<VAR>f : MeasureTheory.Filtration ι m<VAR>Countable ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>PartialOrder ι<VAR>τ : Ω → ι<VAR>f : MeasureTheory.Filtration ι m<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>PartialOrder ι<VAR>τ : Ω → ι<VAR>f : MeasureTheory.Filtration ι m<VAR>Countable ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>ι : Type u_4<VAR>LinearOrder ι<VAR>τ : Ω → ι<VAR>f : MeasureTheory.Filtration ι m<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>ι : Type u_4<VAR>LinearOrder ι<VAR>τ : Ω → ι<VAR>f : MeasureTheory.Filtration ι m<VAR>Countable ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | i < τ ω}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<VAR>h_lub : IsLUB (Set.Iio i) i<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i j : ι<VAR>hle : i ≤ j<GOAL>MeasurableSet {ω | τ ω = i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>TopologicalSpace ι<VAR>OrderTopology ι<VAR>FirstCountableTopology ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i j : ι<VAR>hle : i ≤ j<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>Preorder ι<VAR>Countable ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : ∀ (i : ι), MeasurableSet {ω | τ ω = i}<GOAL>MeasureTheory.IsStoppingTime f τ
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>hπ : MeasureTheory.IsStoppingTime f π<GOAL>MeasureTheory.IsStoppingTime f fun ω => max (τ ω) (π ω)
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ : Ω → ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>i : ι<GOAL>MeasureTheory.IsStoppingTime f fun ω => max (τ ω) i
<VAR>Ω : Type u_1<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>LinearOrder ι<VAR>f : MeasureTheory.Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : MeasureTheory.IsStoppingTime f τ<VAR>hπ : MeasureTheory.IsStoppingTime f π<GOAL>MeasureTheory.IsStoppingTime f fun ω => min (τ ω) (π ω)