ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>IsLocalization N T<VAR>y : ↥(IsLocalization.localizationLocalizationSubmodule M N)<GOAL>IsUnit ((algebraMap R T) ↑y)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>IsLocalization N T<VAR>x : T<GOAL>∃ y, x * (algebraMap R T) ↑y.2 = (algebraMap R T) y.1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>IsLocalization N T<VAR>x y : R<GOAL>(algebraMap R T) x = (algebraMap R T) y → ∃ c, ↑c * x = ↑c * y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>IsLocalization N T<GOAL>IsLocalization (IsLocalization.localizationLocalizationSubmodule M N) T
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>IsLocalization N T<VAR>H : ∀ (x : S), IsUnit x → x ∈ N<GOAL>IsLocalization (Submonoid.comap (algebraMap R S) N) T
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>p : Ideal S<VAR>Hp : p.IsPrime<VAR>IsLocalization.AtPrime T p<GOAL>IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>IsLocalization M S<VAR>IsLocalization N T<GOAL>IsScalarTower R S T
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>T : Type u_4<VAR>CommSemiring T<VAR>Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>IsLocalization M S<VAR>IsLocalization N T<VAR>Algebra S T<VAR>IsScalarTower R S T<GOAL>IsLocalization (Submonoid.map (algebraMap R S) N) T
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>M N : Submonoid R<VAR>IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<GOAL>IsLocalization N S
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_3<VAR>T : Type u_4<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>IsFractionRing R T<VAR>hM : M ≤ nonZeroDivisors R<GOAL>IsFractionRing S T
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>IsDomain R<VAR>S : Type u_3<VAR>T : Type u_4<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>IsLocalization M S<VAR>IsFractionRing R T<GOAL>IsFractionRing S T
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Algebra.FormallyUnramified R S ↔ Subsingleton (Ω[S⁄R])
<VAR>z : ℂ<GOAL>(Algebra.leftMulMatrix Complex.basisOneI) z = !![z.re, -z.im; z.im, z.re]
<VAR>z : ℂ<GOAL>(Algebra.trace ℝ ℂ) z = 2 * z.re
<VAR>z : ℂ<GOAL>(Algebra.norm ℝ) z = Complex.normSq z
<GOAL>Algebra.norm ℝ = ↑Complex.normSq
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>r : S<VAR>x : P.Ring<VAR>i : P.vars<GOAL>(P.cotangentSpaceBasis.repr (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x)) i = r * (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x : P.Ring<VAR>i : P.vars<GOAL>(P.cotangentSpaceBasis.repr (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x)) i = (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv i) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>i : P.vars<GOAL>P.cotangentSpaceBasis i = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) (MvPolynomial.X i)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x : ↥P.ker<GOAL>P.cotangentComplex (Algebra.Generators.Cotangent.mk x) = 1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>x : S<VAR>y : P.Ring<GOAL>(Algebra.Generators.CotangentSpace.map f) (x ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) y) = (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.D R' P'.Ring) (f.toAlgHom y)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>i : P.vars<VAR>j : P'.vars<GOAL>(P'.cotangentSpaceBasis.repr ((Algebra.Generators.CotangentSpace.map f) (P.cotangentSpaceBasis i))) j = (MvPolynomial.aeval P'.val) ((MvPolynomial.pderiv j) (f.val i))
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Algebra.Generators.CotangentSpace.map (Algebra.Generators.Hom.id P) = LinearMap.id
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>CommRing R''<VAR>CommRing S''<VAR>Algebra R'' S''<VAR>P'' : Algebra.Generators R'' S''<VAR>Algebra R R''<VAR>Algebra S S''<VAR>Algebra R S''<VAR>IsScalarTower R R'' S''<VAR>IsScalarTower R S S''<VAR>Algebra R' R''<VAR>Algebra S' S''<VAR>Algebra R' S''<VAR>IsScalarTower R' R'' S''<VAR>IsScalarTower R' S' S''<VAR>IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<GOAL>Algebra.Generators.CotangentSpace.map (g.comp f) = ↑S (Algebra.Generators.CotangentSpace.map g) ∘ₗ Algebra.Generators.CotangentSpace.map f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>CommRing R''<VAR>CommRing S''<VAR>Algebra R'' S''<VAR>P'' : Algebra.Generators R'' S''<VAR>Algebra R R''<VAR>Algebra S S''<VAR>Algebra R S''<VAR>IsScalarTower R R'' S''<VAR>IsScalarTower R S S''<VAR>Algebra R' R''<VAR>Algebra S' S''<VAR>Algebra R' S''<VAR>IsScalarTower R' R'' S''<VAR>IsScalarTower R' S' S''<VAR>IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<VAR>x : P.CotangentSpace<GOAL>(Algebra.Generators.CotangentSpace.map (g.comp f)) x = (Algebra.Generators.CotangentSpace.map g) ((Algebra.Generators.CotangentSpace.map f) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>x : P.Cotangent<GOAL>(Algebra.Generators.CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Algebra.Generators.Cotangent.map f) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<GOAL>Algebra.Generators.CotangentSpace.map f ∘ₗ P.cotangentComplex = ↑S P'.cotangentComplex ∘ₗ Algebra.Generators.Cotangent.map f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f g : P.Hom P'<VAR>x y : P.Ring<GOAL>f.toAlgHom (x * y) - g.toAlgHom (x * y) - (P'.σ ((algebraMap P.Ring S') x) * (f.toAlgHom y - g.toAlgHom y) + P'.σ ((algebraMap P.Ring S') y) * (f.toAlgHom x - g.toAlgHom x)) ∈ P'.ker ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f g : P.Hom P'<VAR>c : P.Ring<GOAL>↑((f.subToKer g) c) = f.toAlgHom c - g.toAlgHom c
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f g : P.Hom P'<VAR>x : P.Ring<GOAL>(f.sub g) (1 ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = Algebra.Generators.Cotangent.mk ((f.subToKer g) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f g : P.Hom P'<VAR>r : S<VAR>x : P.Ring<GOAL>(f.sub g) (r ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) x) = r • Algebra.Generators.Cotangent.mk ((f.subToKer g) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f g : P.Hom P'<GOAL>Algebra.Generators.CotangentSpace.map f - Algebra.Generators.CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f g : P.Hom P'<GOAL>Algebra.Generators.Cotangent.map f - Algebra.Generators.Cotangent.map g = f.sub g ∘ₗ P.cotangentComplex
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>i : P.vars<GOAL>P.toKaehler (P.cotangentSpaceBasis i) = (KaehlerDifferential.D R S) (P.val i)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Function.Surjective ⇑P.toKaehler
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Function.Exact ⇑P.cotangentComplex ⇑P.toKaehler
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.FormallyEtale R A ↔ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.FormallyEtale R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>I : Ideal B<GOAL>I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.FormallyEtale R A ↔ Algebra.FormallyUnramified R A ∧ Algebra.FormallySmooth R A
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>h₁ : Algebra.FormallyUnramified R A<VAR>h₂ : Algebra.FormallySmooth R A<GOAL>Algebra.FormallyEtale R A
<VAR>R : Type u<VAR>CommSemiring R<VAR>A B : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra.FormallyEtale R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.FormallyEtale R B
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>CommSemiring A<VAR>Algebra R A<VAR>B : Type u<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.FormallyEtale R A<VAR>Algebra.FormallyEtale A B<GOAL>Algebra.FormallyEtale R B
<VAR>R Rₘ : Type u<VAR>CommRing R<VAR>CommRing Rₘ<VAR>M : Submonoid R<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<GOAL>Algebra.FormallyEtale R Rₘ
<VAR>R Rₘ Sₘ : Type u<VAR>CommRing R<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>M : Submonoid R<VAR>Algebra R Sₘ<VAR>Algebra R Rₘ<VAR>Algebra Rₘ Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsLocalization M Rₘ<VAR>Algebra.FormallyEtale R Sₘ<GOAL>Algebra.FormallyEtale Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>M : Submonoid R<VAR>Algebra R S<VAR>Algebra R Sₘ<VAR>Algebra S Sₘ<VAR>Algebra R Rₘ<VAR>Algebra Rₘ Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>IsLocalization M Rₘ<VAR>IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Algebra.FormallyEtale R S<GOAL>Algebra.FormallyEtale Rₘ Sₘ
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.Etale R A<GOAL>Algebra.FinitePresentation R A
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.Etale R A<GOAL>Algebra.FormallyEtale R A
<VAR>R : Type u<VAR>CommRing R<VAR>A B : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.Etale R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.Etale R B
<VAR>R : Type u<VAR>CommRing R<VAR>A B : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.Etale R A<VAR>Algebra.Etale A B<GOAL>Algebra.Etale R B
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>r : R<VAR>IsLocalization.Away r A<GOAL>Algebra.Etale R A
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<GOAL>N = J • N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N = I • N<VAR>hIjac : I ≤ N.annihilator.jacobson<GOAL>N = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hrN : N = r • N<VAR>hrJac : r ∈ N.annihilator.jacobson<GOAL>N = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Set R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hsN : N = s • N<VAR>hsJac : s ⊆ ↑N.annihilator.jacobson<GOAL>N = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial M<VAR>Module.Finite R M<VAR>I : Ideal R<VAR>h : I ≤ (Module.annihilator R M).jacobson<GOAL>⊤ ≠ I • ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial M<VAR>Module.Finite R M<VAR>s : Set R<VAR>h : s ⊆ ↑(Module.annihilator R M).jacobson<GOAL>⊤ ≠ s • ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial M<VAR>Module.Finite R M<VAR>r : R<VAR>h : r ∈ (Module.annihilator R M).jacobson<GOAL>⊤ ≠ r • ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ ⊥.jacobson<GOAL>N = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I J : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ J.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<GOAL>N ⊔ N' = N ⊔ J • N'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I J : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ J.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<GOAL>N ⊔ I • N' = N ⊔ J • N'
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ ⊥.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<GOAL>N' ≤ N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N N' : Submodule R M<VAR>hN' : N'.FG<VAR>hIJ : I ≤ ⊥.jacobson<VAR>hNN : N' ≤ N ⊔ I • N'<GOAL>I • N' ≤ N
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x : R<GOAL>x ∈ I ↔ I.ringCon x 0
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<GOAL>I.ringCon x y ↔ x - y ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<GOAL>∀ (a : TwoSidedIdeal R), TwoSidedIdeal.coeOrderEmbedding a = ↑a
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<GOAL>I ≤ J ↔ ↑I ⊆ ↑J
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<GOAL>Function.Injective TwoSidedIdeal.ringCon
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<GOAL>I ≤ J ↔ I.ringCon ≤ J.ringCon
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<VAR>h : ∀ (x : R), x ∈ I ↔ x ∈ J<GOAL>I = J
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<GOAL>I < J ↔ ↑I ⊂ ↑J
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<GOAL>0 ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<VAR>hx : x ∈ I<VAR>hy : y ∈ I<GOAL>x + y ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x : R<VAR>hx : x ∈ I<GOAL>-x ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<VAR>hx : x ∈ I<VAR>hy : y ∈ I<GOAL>x - y ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<VAR>hy : y ∈ I<GOAL>x * y ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<VAR>hx : x ∈ I<GOAL>x * y ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x : R<VAR>n : ℕ<VAR>hx : x ∈ I<GOAL>n • x ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x : R<VAR>n : ℤ<VAR>hx : x ∈ I<GOAL>n • x ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>carrier : Set R<VAR>zero_mem : 0 ∈ carrier<VAR>add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier<VAR>neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier<VAR>mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier<VAR>mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier<VAR>x : R<GOAL>x ∈ TwoSidedIdeal.mk' carrier zero_mem ⋯ ⋯ ⋯ ⋯ ↔ x ∈ carrier
<VAR>R : Type u_1<VAR>Ring R<VAR>I : TwoSidedIdeal R<VAR>r : R<VAR>x : ↥I<GOAL>r • ↑x = r * ↑x
<VAR>R : Type u_1<VAR>Ring R<VAR>I : TwoSidedIdeal R<VAR>r : Rᵐᵒᵖ<VAR>x : ↥I<GOAL>r • ↑x = ↑x * MulOpposite.unop r
<VAR>R : Type u_1<VAR>Ring R<VAR>I : TwoSidedIdeal R<VAR>x : ↥I<GOAL>I.subtype x = ↑x
<VAR>R : Type u_1<VAR>Ring R<VAR>I : TwoSidedIdeal R<VAR>x : ↥I<GOAL>I.subtypeMop x = MulOpposite.op ↑x
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.FormallyUnramified R A ↔ ∀ ⦃B : Type u⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B), I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.FormallyUnramified R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>I : Ideal B<GOAL>I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>_RB : Algebra R B<VAR>Algebra.FormallyUnramified R A<VAR>I : Ideal B<VAR>hI : IsNilpotent I<VAR>g₁ g₂ : A →ₐ[R] B<VAR>h : (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂<GOAL>g₁ = g₂
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>I : Ideal B<VAR>Algebra.FormallyUnramified R A<VAR>hI : IsNilpotent I<VAR>g₁ g₂ : A →ₐ[R] B<VAR>H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)<GOAL>g₁ = g₂
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.FormallyUnramified R A<VAR>C : Type u<VAR>CommRing C<VAR>f : B →+* C<VAR>hf : IsNilpotent (RingHom.ker f)<VAR>g₁ g₂ : A →ₐ[R] B<VAR>h : f.comp ↑g₁ = f.comp ↑g₂<GOAL>g₁ = g₂
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.FormallyUnramified R A<VAR>C : Type u<VAR>CommRing C<VAR>f : B →+* C<VAR>hf : IsNilpotent (RingHom.ker f)<VAR>g₁ g₂ : A →ₐ[R] B<VAR>h : ∀ (x : A), f (g₁ x) = f (g₂ x)<GOAL>g₁ = g₂
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>B : Type u<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.FormallyUnramified R A<VAR>C : Type u<VAR>CommRing C<VAR>Algebra R C<VAR>f : B →ₐ[R] C<VAR>hf : IsNilpotent (RingHom.ker ↑f)<VAR>g₁ g₂ : A →ₐ[R] B<VAR>h : f.comp g₁ = f.comp g₂<GOAL>g₁ = g₂
<VAR>R : Type u<VAR>CommSemiring R<VAR>A B : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra.FormallyUnramified R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.FormallyUnramified R B
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>CommSemiring A<VAR>Algebra R A<VAR>B : Type u<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.FormallyUnramified R A<VAR>Algebra.FormallyUnramified A B<GOAL>Algebra.FormallyUnramified R B
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>CommSemiring A<VAR>Algebra R A<VAR>B : Type u<VAR>Semiring B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.FormallyUnramified R B<GOAL>Algebra.FormallyUnramified A B
<VAR>R Rₘ : Type u<VAR>CommRing R<VAR>CommRing Rₘ<VAR>M : Submonoid R<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<GOAL>Algebra.FormallyUnramified R Rₘ
<VAR>R Rₘ Sₘ : Type u<VAR>CommRing R<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>M : Submonoid R<VAR>Algebra R Sₘ<VAR>Algebra R Rₘ<VAR>Algebra Rₘ Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>Algebra.FormallyUnramified R Sₘ<GOAL>Algebra.FormallyUnramified Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>M : Submonoid R<VAR>Algebra R S<VAR>Algebra R Sₘ<VAR>Algebra S Sₘ<VAR>Algebra R Rₘ<VAR>Algebra Rₘ Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>Algebra.FormallyUnramified R S<GOAL>Algebra.FormallyUnramified Rₘ Sₘ
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.Unramified R A<GOAL>Algebra.FiniteType R A
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type u<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.Unramified R A<GOAL>Algebra.FormallyUnramified R A
<VAR>R : Type u<VAR>CommRing R<VAR>A B : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.Unramified R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.Unramified R B
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u<VAR>CommRing A<VAR>Algebra R A<VAR>r : R<VAR>IsLocalization.Away r A<GOAL>Algebra.Unramified R A