ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>CommRing Sₘ<VAR>Algebra S Sₘ<VAR>M : Submonoid R<VAR>IsLocalization M Rₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>a : S<VAR>b : R<VAR>hM : M ≤ R⁰<GOAL>(Algebra.norm R) a = b ↔ (Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>CommRing Sₘ<VAR>Algebra S Sₘ<VAR>M : Submonoid R<VAR>IsLocalization M Rₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>a : S<GOAL>(Algebra.trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((Algebra.trace R S) a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_3<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>M : Submonoid R<VAR>IsLocalization M Rₘ<VAR>Sₘ : Type u_5<VAR>CommRing Sₘ<VAR>Algebra S Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R S<GOAL>Algebra.traceMatrix Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (Algebra.traceMatrix R ⇑b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Rₘ : Type u_3<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>M : Submonoid R<VAR>IsLocalization M Rₘ<VAR>Sₘ : Type u_5<VAR>CommRing Sₘ<VAR>Algebra S Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>ι : Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι R S<GOAL>Algebra.discr Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (Algebra.discr R ⇑b)
<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>r : AdicCompletion I R<VAR>x : M<GOAL>((AdicCompletion.ofTensorProductBil I M) r) x = r • (AdicCompletion.of 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>r : AdicCompletion I R<VAR>x : M<GOAL>(AdicCompletion.ofTensorProduct I M) (r ⊗ₜ[R] x) = r • (AdicCompletion.of 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>N : Type u_3<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<GOAL>AdicCompletion.map I f ∘ₗ AdicCompletion.ofTensorProduct I M = AdicCompletion.ofTensorProduct I N ∘ₗ TensorProduct.AlgebraTensorModule.map LinearMap.id f
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<GOAL>↑(AdicCompletion.piEquivOfFintype I fun x => R) ∘ₗ AdicCompletion.ofTensorProduct I (ι → R) = ↑(TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<GOAL>AdicCompletion.ofTensorProduct I (ι → R) = ↑(AdicCompletion.piEquivOfFintype I fun x => R).symm ∘ₗ ↑(TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<GOAL>↑(AdicCompletion.ofTensorProductInvOfPiFintype I ι) ∘ₗ AdicCompletion.ofTensorProduct I (ι → R) = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<GOAL>AdicCompletion.ofTensorProduct I (ι → R) ∘ₗ ↑(AdicCompletion.ofTensorProductInvOfPiFintype I ι) = LinearMap.id
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_4<VAR>Finite ι<GOAL>Function.Bijective ⇑(AdicCompletion.ofTensorProduct I (ι → R))
<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>Module.Finite R M<GOAL>Function.Surjective ⇑(AdicCompletion.ofTensorProduct I M)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type<VAR>f : (ι → R) →ₗ[R] M<GOAL>Function.Exact ⇑(LinearMap.ker f).subtype ⇑f
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Exact ⇑(AdicCompletion.lTensorKerIncl I M f) ⇑(AdicCompletion.lTensorf I M f)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(AdicCompletion.lTensorf I M f)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>ι : Type<VAR>Fintype ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Exact ⇑(AdicCompletion.map I (LinearMap.ker f).subtype) ⇑(AdicCompletion.map I f)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(AdicCompletion.map I f)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>(AdicCompletion.firstRow I M f).Exact
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>ι : Type<VAR>Fintype ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>(AdicCompletion.secondRow I M f).Exact
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>ι : Type<VAR>Fintype ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>CategoryTheory.IsIso (ModuleCat.ofHom (AdicCompletion.ofTensorProduct I M))
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>ι : Type<VAR>Fintype ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Bijective ⇑(AdicCompletion.ofTensorProduct I M)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>Module.Finite R M<GOAL>Function.Bijective ⇑(AdicCompletion.ofTensorProduct I M)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>Module.Finite R M<VAR>x : AdicCompletion I R ⊗[R] M<GOAL>(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M) x = (AdicCompletion.ofTensorProduct I M) x
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>Module.Finite R M<VAR>x : M<GOAL>(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M).symm ((AdicCompletion.of I M) x) = 1 ⊗ₜ[R] x
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>Module.Finite R M<VAR>Module.Finite R N<GOAL>TensorProduct.AlgebraTensorModule.map LinearMap.id f = ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ AdicCompletion.map I f ∘ₗ ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>Module.Finite R M<VAR>Module.Finite R N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(TensorProduct.AlgebraTensorModule.map LinearMap.id f)
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<GOAL>∃ a b, IsRelPrime a ↑b ∧ IsLocalization.mk' K a b = x
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<GOAL>IsRelPrime (IsFractionRing.num A x) ↑(IsFractionRing.den A x)
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<GOAL>IsLocalization.mk' K (IsFractionRing.num A x) (IsFractionRing.den A x) = x
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<GOAL>(algebraMap A K) (IsFractionRing.num A x) / (algebraMap A K) ↑(IsFractionRing.den A x) = x
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x y : K<GOAL>x * (algebraMap A K) ↑(IsFractionRing.den A y) = (algebraMap A K) (IsFractionRing.num A y) ↔ x = y
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x y : K<GOAL>y * (algebraMap A K) ↑(IsFractionRing.den A x) = (algebraMap A K) (IsFractionRing.num A x) ↔ x = y
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x y : K<GOAL>IsFractionRing.num A y * ↑(IsFractionRing.den A x) = IsFractionRing.num A x * ↑(IsFractionRing.den A y) ↔ x = y
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<VAR>h : IsFractionRing.num A x = 0<GOAL>x = 0
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<GOAL>IsFractionRing.num A 0 = 0
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<GOAL>IsFractionRing.num A x = 0 ↔ x = 0
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<VAR>h : IsUnit ↑(IsFractionRing.den A x)<GOAL>IsLocalization.IsInteger A x
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<GOAL>IsUnit ↑(IsFractionRing.den A x) ↔ IsLocalization.IsInteger A x
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<GOAL>IsUnit ↑(IsFractionRing.den A 0)
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<VAR>h : IsFractionRing.num A x = 0<GOAL>IsUnit ↑(IsFractionRing.den A x)
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>Associated (↑(IsFractionRing.den A x)) (IsFractionRing.num A x⁻¹)
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>Associated (IsFractionRing.num A x) ↑(IsFractionRing.den A x⁻¹)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<GOAL>Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<GOAL>Function.Surjective ⇑(IsLocalization.toInvSubmonoid M S)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>m : ↥M<GOAL>↑((IsLocalization.toInvSubmonoid M S) m) * (algebraMap R S) ↑m = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>m : ↥M<GOAL>(algebraMap R S) ↑m * ↑((IsLocalization.toInvSubmonoid M S) m) = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>m : ↥M<GOAL>m • ↑((IsLocalization.toInvSubmonoid M S) m) = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>z : S<GOAL>∃ r m, z = r • ↑((IsLocalization.toInvSubmonoid M S) m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>x : ↥M<GOAL>↑((IsLocalization.toInvSubmonoid M S) x) = IsLocalization.mk' S 1 x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>x : S<GOAL>x ∈ IsLocalization.invSubmonoid M S ↔ ∃ m, IsLocalization.mk' S 1 m = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<GOAL>Submodule.span R ↑(IsLocalization.invSubmonoid M S) = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>Monoid.FG ↥M<GOAL>Algebra.FiniteType R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.Presentation R S<GOAL>Ideal.span (Set.range self.relation) = self.ker
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Presentation R S<VAR>i : P.rels<GOAL>(MvPolynomial.aeval P.val) (P.relation i) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Presentation R S<VAR>p : P.Ring<GOAL>P.quotientEquiv ((Ideal.Quotient.mk P.ker) p) = (algebraMap P.Ring S) p
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Presentation R S<VAR>x : S<GOAL>P.quotientEquiv.symm x = (Ideal.Quotient.mk P.ker) (P.σ x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Presentation R S<VAR>self : P.IsFinite<GOAL>Finite P.rels
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Presentation R S<VAR>self : P.IsFinite<GOAL>Finite P.vars
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Presentation R S<VAR>P.IsFinite<GOAL>P.ker.FG
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Presentation R S<VAR>P.IsFinite<GOAL>Algebra.FinitePresentation R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1} = RingHom.ker (MvPolynomial.aeval (Algebra.Generators.localizationAway r).val)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>∀ (x : Unit), (Algebra.Presentation.localizationAway r).relation x = MvPolynomial.C r * MvPolynomial.X () - 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>(Algebra.Presentation.localizationAway r).rels = Unit
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>(Algebra.Presentation.localizationAway r).dimension = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>P : Algebra.Presentation R S<GOAL>Ideal.span (Set.range fun i => (MvPolynomial.map (algebraMap R T)) (P.relation i)) = RingHom.ker (MvPolynomial.aeval P.baseChange.val)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>P : Algebra.Presentation R S<VAR>i : P.rels<GOAL>P.baseChange.relation i = (MvPolynomial.map (algebraMap R T)) (P.relation i)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>P : Algebra.Presentation R S<GOAL>P.baseChange.rels = P.rels
<VAR>R : Type w₁<VAR>CommRing R<VAR>A : Type w₂<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type w₃<VAR>CommRing B<VAR>Algebra R B<VAR>σ : Type u_1<VAR>f : MvPolynomial σ R →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(Algebra.TensorProduct.map (AlgHom.id B B) f)
<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>IsLocalization M S<VAR>I : Ideal R<VAR>z : S<GOAL>z ∈ Ideal.map (algebraMap R S) I ↔ ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.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>IsLocalization M S<VAR>I : Ideal R<VAR>x : R<VAR>s : ↥M<GOAL>IsLocalization.mk' S x s ∈ Ideal.map (algebraMap R S) I ↔ ∃ s ∈ M, s * x ∈ I
<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>IsLocalization M S<VAR>J : Ideal S<GOAL>Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J) = J
<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>IsLocalization M S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>hM : Disjoint ↑M ↑I<GOAL>Ideal.comap (algebraMap R S) (Ideal.map (algebraMap R S) I) = I
<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>IsLocalization M S<VAR>J : Ideal S<GOAL>J.IsPrime ↔ (Ideal.comap (algebraMap R S) J).IsPrime ∧ Disjoint ↑M ↑(Ideal.comap (algebraMap R S) J)
<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>IsLocalization M S<VAR>I : Ideal R<VAR>hp : I.IsPrime<VAR>hd : Disjoint ↑M ↑I<GOAL>(Ideal.map (algebraMap R S) I).IsPrime
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>I : Ideal S<VAR>I.IsPrime<VAR>J : Ideal R<VAR>H : J ≤ Ideal.comap (algebraMap R S) I<VAR>hI : (Ideal.comap (algebraMap R S) I).IsMaximal<GOAL>Function.Surjective ⇑(Ideal.quotientMap I (algebraMap R S) H)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>IsDomain R<VAR>hM : M ≤ nonZeroDivisors R<VAR>p : Ideal S<VAR>hpp : p.IsPrime<VAR>hp0 : p ≠ ⊥<GOAL>⊥ < Ideal.comap (algebraMap R S) p
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>I : Ideal R<GOAL>I = ⨅ f ∈ S, Ideal.comap (algebraMap R (Localization.Away f)) (Ideal.map (algebraMap R (Localization.Away f)) I)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>S : Submonoid A<VAR>CommRing K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>hS : S ≤ nonZeroDivisors A<VAR>s : ↥S<GOAL>IsUnit ((algebraMap A K) ↑s)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>S : Submonoid A<VAR>CommRing K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra A B<VAR>IsLocalization S B<VAR>hS : S ≤ nonZeroDivisors A<VAR>b : B<GOAL>(Localization.mapToFractionRing K S B hS) b = (IsLocalization.lift ⋯) b
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>S : Submonoid A<VAR>CommRing K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra A B<VAR>IsLocalization S B<VAR>hS : S ≤ nonZeroDivisors A<VAR>x : K<GOAL>x ∈ (Localization.mapToFractionRing K S B hS).range ↔ ∃ a s, ∃ (hs : s ∈ S), x = IsLocalization.mk' K a ⟨s, ⋯⟩
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>CommRing A<VAR>S : Submonoid A<VAR>hS : S ≤ nonZeroDivisors A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra A B<VAR>IsLocalization S B<VAR>x : K<GOAL>x ∈ (Localization.mapToFractionRing K S B hS).range ↔ ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹
<VAR>R : Type u<VAR>CommRing R<VAR>S : Submonoid R<VAR>L : Type u<VAR>CommRing L<VAR>Algebra R L<VAR>IsLocalization S L<GOAL>#L ≤ #R
<VAR>R : Type u<VAR>CommRing R<VAR>S : Submonoid R<VAR>L : Type u<VAR>CommRing L<VAR>Algebra R L<VAR>IsLocalization S L<VAR>hS : S ≤ R⁰<GOAL>#R = #L
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b<GOAL>LocalRing R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R<GOAL>LocalRing R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>h : ∃! I, I.IsMaximal<GOAL>LocalRing R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>h : ∃! P, P ≠ ⊥ ∧ P.IsPrime<GOAL>LocalRing R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>LocalRing R<VAR>a b : R<VAR>h : IsUnit (a + b)<GOAL>IsUnit a ∨ IsUnit b
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>LocalRing R<VAR>a b : R<VAR>ha : a ∈ nonunits R<VAR>hb : b ∈ nonunits R<GOAL>a + b ∈ nonunits R
<VAR>R : Type u_1<VAR>CommRing R<VAR>Nontrivial R<VAR>h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a)<GOAL>LocalRing R
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>a : R<GOAL>IsUnit a ∨ IsUnit (1 - a)
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>a : R<VAR>h : 1 - a ∈ nonunits R<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>a : R<VAR>h : a ∈ nonunits R<GOAL>IsUnit (1 - a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>Nontrivial S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>LocalRing S
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>x : R<VAR>IsLocalization.Away x S<GOAL>(algebraMap R S) x * IsLocalization.Away.invSelf x = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>x : R<VAR>IsLocalization.Away x S<VAR>s : S<GOAL>s * (algebraMap R S) (x ^ (IsLocalization.Away.sec x s).2) = (algebraMap R S) (IsLocalization.Away.sec x s).1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>P : Type u_3<VAR>CommSemiring P<VAR>x : R<VAR>IsLocalization.Away x S<VAR>g : R →+* P<VAR>hg : IsUnit (g x)<VAR>a : R<GOAL>(IsLocalization.Away.lift x hg) ((algebraMap R S) a) = g a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>P : Type u_3<VAR>CommSemiring P<VAR>x : R<VAR>IsLocalization.Away x S<VAR>g : R →+* P<VAR>hg : IsUnit (g x)<GOAL>(IsLocalization.Away.lift x hg).comp (algebraMap R S) = g
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type u_6<VAR>CommRing B<VAR>Algebra R B<VAR>Aₚ : Type u_7<VAR>CommRing Aₚ<VAR>Algebra A Aₚ<VAR>Algebra R Aₚ<VAR>IsScalarTower R A Aₚ<VAR>Bₚ : Type u_8<VAR>CommRing Bₚ<VAR>Algebra B Bₚ<VAR>Algebra R Bₚ<VAR>IsScalarTower R B Bₚ<VAR>f : A →ₐ[R] B<VAR>a : A<VAR>IsLocalization.Away a Aₚ<VAR>IsLocalization.Away (f a) Bₚ<VAR>x : Aₚ<GOAL>(IsLocalization.Away.mapₐ Aₚ Bₚ f a) x = (IsLocalization.Away.map Aₚ Bₚ f.toRingHom a) x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type u_6<VAR>CommRing B<VAR>Algebra R B<VAR>Aₚ : Type u_7<VAR>CommRing Aₚ<VAR>Algebra A Aₚ<VAR>Algebra R Aₚ<VAR>IsScalarTower R A Aₚ<VAR>Bₚ : Type u_8<VAR>CommRing Bₚ<VAR>Algebra B Bₚ<VAR>Algebra R Bₚ<VAR>IsScalarTower R B Bₚ<VAR>f : A →ₐ[R] B<VAR>a : A<VAR>IsLocalization.Away a Aₚ<VAR>IsLocalization.Away (f a) Bₚ<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(IsLocalization.Away.mapₐ Aₚ Bₚ f a)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type u_6<VAR>CommRing B<VAR>Algebra R B<VAR>Aₚ : Type u_7<VAR>CommRing Aₚ<VAR>Algebra A Aₚ<VAR>Algebra R Aₚ<VAR>IsScalarTower R A Aₚ<VAR>Bₚ : Type u_8<VAR>CommRing Bₚ<VAR>Algebra B Bₚ<VAR>Algebra R Bₚ<VAR>IsScalarTower R B Bₚ<VAR>f : A →ₐ[R] B<VAR>a : A<VAR>IsLocalization.Away a Aₚ<VAR>IsLocalization.Away (f a) Bₚ<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(IsLocalization.Away.mapₐ Aₚ Bₚ f a)