ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.Unramified R A<VAR>Algebra.Unramified A B<GOAL>Algebra.Unramified R B
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set (σ →₀ ℕ)<GOAL>x ∈ Ideal.span ((fun s => (MvPolynomial.monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set (σ →₀ ℕ)<GOAL>x ∈ Ideal.span ((fun s => (MvPolynomial.monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, (MvPolynomial.monomial si) 1 ∣ (MvPolynomial.monomial xi) (MvPolynomial.coeff xi x)
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set σ<GOAL>x ∈ Ideal.span (MvPolynomial.X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
<VAR>σ : Type u<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<GOAL>Finsupp.mapRange ⇑f ⋯ p = (MvPolynomial.map f) p
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<VAR>s t : Set (σ →₀ ℕ)<VAR>h : s ⊆ t<GOAL>MvPolynomial.restrictSupport R s ≤ MvPolynomial.restrictSupport R t
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<VAR>m : ℕ<VAR>p : MvPolynomial σ R<GOAL>p ∈ MvPolynomial.restrictTotalDegree σ R m ↔ p.totalDegree ≤ m
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>p ∈ MvPolynomial.restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>p ∈ MvPolynomial.restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i p.degrees ≤ n
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<VAR>m : ℕ<GOAL>MvPolynomial.restrictTotalDegree σ R m ≤ MvPolynomial.restrictDegree σ R m
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<GOAL>⇑(MvPolynomial.basisMonomials σ R) = fun s => (MvPolynomial.monomial s) 1
<VAR>σ : Type u<VAR>R : Type v<VAR>CommSemiring R<GOAL>LinearIndependent R MvPolynomial.X
<VAR>α : Type u_1<VAR>Finite α<VAR>n : ℕ<GOAL>Finite ↑{f | ∀ (a : α), f a ≤ n}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>σ : Type u_3<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<GOAL>algebraMap (MvPolynomial σ R) (MvPolynomial σ S) = MvPolynomial.map (algebraMap R S)
<VAR>R : Type v<VAR>CommSemiring R<GOAL>⇑(Polynomial.basisMonomials R) = fun s => (Polynomial.monomial s) 1
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<GOAL>(I ⊔ J).ringCon = I.ringCon ⊔ J.ringCon
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<VAR>x : R<VAR>h : x ∈ I<GOAL>x ∈ I ⊔ J
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<VAR>x : R<VAR>h : x ∈ J<GOAL>x ∈ I ⊔ J
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<VAR>x : R<GOAL>x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<GOAL>(I ⊓ J).ringCon = I.ringCon ⊓ J.ringCon
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>I J : TwoSidedIdeal R<VAR>x : R<GOAL>x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>S : Set (TwoSidedIdeal R)<GOAL>(sSup S).ringCon = sSup (TwoSidedIdeal.ringCon '' S)
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>ι : Type u_2<VAR>I : ι → TwoSidedIdeal R<GOAL>(⨆ i, I i).ringCon = ⨆ i, (I i).ringCon
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>S : Set (TwoSidedIdeal R)<GOAL>(sInf S).ringCon = sInf (TwoSidedIdeal.ringCon '' S)
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>ι : Type u_2<VAR>I : ι → TwoSidedIdeal R<GOAL>(⨅ i, I i).ringCon = ⨅ i, (I i).ringCon
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>ι : Type u_2<VAR>I : ι → TwoSidedIdeal R<VAR>x : R<GOAL>x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>S : Set (TwoSidedIdeal R)<VAR>x : R<GOAL>x ∈ sInf S ↔ ∀ I ∈ S, x ∈ I
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<GOAL>⊤.ringCon = ⊤
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<GOAL>⊥.ringCon = ⊥
<VAR>R : Type u_1<VAR>NonUnitalNonAssocRing R<VAR>x : R<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>x : σ → B<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval x) ((MvPolynomial.map (algebraMap R A)) p) = (MvPolynomial.aeval x) p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>x : σ → A<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval (⇑(algebraMap A B) ∘ x)) p = (algebraMap A B) ((MvPolynomial.aeval x) p)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>NoZeroSMulDivisors A B<VAR>Nontrivial B<VAR>x : σ → A<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (MvPolynomial.aeval x) p = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>σ : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Algebra R A<VAR>Algebra A B<VAR>Algebra R B<VAR>IsScalarTower R A B<VAR>x : σ → A<VAR>p : MvPolynomial σ R<VAR>h : Function.Injective ⇑(algebraMap A B)<GOAL>(MvPolynomial.aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (MvPolynomial.aeval x) p = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>σ : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>x : σ → ↥S<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.aeval fun i => ↑(x i)) p = ↑((MvPolynomial.aeval x) p)
<VAR>ι : Type u_1<VAR>S : Type u_2<VAR>AddMonoid S<VAR>Mul S<VAR>t : RingCon S<VAR>l : List ι<VAR>f g : ι → S<VAR>h : ∀ i ∈ l, t (f i) (g i)<GOAL>t (List.map f l).sum (List.map g l).sum
<VAR>ι : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Mul S<VAR>t : RingCon S<VAR>s : Multiset ι<VAR>f g : ι → S<VAR>h : ∀ i ∈ s, t (f i) (g i)<GOAL>t (Multiset.map f s).sum (Multiset.map g s).sum
<VAR>ι : Type u_1<VAR>S : Type u_2<VAR>AddCommMonoid S<VAR>Mul S<VAR>t : RingCon S<VAR>s : Finset ι<VAR>f g : ι → S<VAR>h : ∀ i ∈ s, t (f i) (g i)<GOAL>t (s.sum f) (s.sum g)
<VAR>R : Type u_3<VAR>CommRing R<VAR>self : Ideal.IsJacobson R<VAR>I : Ideal R<GOAL>I.IsRadical → I.jacobson = I
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Ideal.IsJacobson R ↔ ∀ (I : Ideal R), I.IsRadical → I.jacobson = I
<VAR>R : Type u_3<VAR>CommRing R<GOAL>Ideal.IsJacobson R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Ideal.IsJacobson R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Ideal.IsJacobson R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Ideal.IsJacobson R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M, (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M
<VAR>R : Type u_1<VAR>CommRing R<VAR>H : Ideal.IsJacobson R<VAR>I : Ideal R<GOAL>I.radical = I.jacobson
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>H : Ideal.IsJacobson R<GOAL>(∃ f, Function.Surjective ⇑f) → Ideal.IsJacobson S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>e : R ≃+* S<GOAL>Ideal.IsJacobson R ↔ Ideal.IsJacobson S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>hR : Ideal.IsJacobson R<GOAL>Ideal.IsJacobson S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : f.IsIntegral<VAR>hR : Ideal.IsJacobson R<GOAL>Ideal.IsJacobson S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>y : R<VAR>Algebra R S<VAR>IsLocalization.Away y S<VAR>H : Ideal.IsJacobson R<VAR>J : Ideal S<GOAL>J.IsMaximal ↔ (Ideal.comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>y : R<VAR>Algebra R S<VAR>IsLocalization.Away y S<VAR>Ideal.IsJacobson R<VAR>I : Ideal R<VAR>hI : I.IsMaximal<VAR>hy : y ∉ I<GOAL>(Ideal.map (algebraMap R S) I).IsMaximal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>y : R<VAR>Algebra R S<VAR>IsLocalization.Away y S<VAR>H : Ideal.IsJacobson R<GOAL>Ideal.IsJacobson S
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>CommRing S<VAR>CommRing T<VAR>g : S →+* T<VAR>u : Set S<VAR>x : S<VAR>hx : x ∈ Subring.closure u<GOAL>g x ∈ Subring.closure (⇑g '' u)
<VAR>R : Type u_1<VAR>Ring R<VAR>p : Polynomial R<GOAL>p ∈ Subring.closure (insert Polynomial.X {f | f.degree ≤ 0})
<VAR>R : Type u_1<VAR>CommRing R<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>P : Ideal (Polynomial R)<VAR>pX : Polynomial R<VAR>hpX : pX ∈ P<VAR>Algebra (R ⧸ Ideal.comap Polynomial.C P) Rₘ<VAR>IsLocalization.Away (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff Rₘ<VAR>Algebra (Polynomial R ⧸ P) Sₘ<VAR>IsLocalization (Submonoid.map (Ideal.quotientMap P Polynomial.C ⋯) (Submonoid.powers (Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) pX).leadingCoeff)) Sₘ<GOAL>(IsLocalization.map Sₘ (Ideal.quotientMap P Polynomial.C ⋯) ⋯).IsIntegral
<VAR>S : Type u_2<VAR>CommRing S<VAR>IsDomain S<VAR>R : Type u_5<VAR>CommRing R<VAR>IsDomain R<VAR>Ideal.IsJacobson R<VAR>Rₘ : Type u_6<VAR>Sₘ : Type u_7<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>φ : R →+* S<VAR>hφ : Function.Injective ⇑φ<VAR>x : R<VAR>hx : x ≠ 0<VAR>Algebra R Rₘ<VAR>IsLocalization.Away x Rₘ<VAR>Algebra S Sₘ<VAR>IsLocalization (Submonoid.map φ (Submonoid.powers x)) Sₘ<VAR>hφ' : (IsLocalization.map Sₘ φ ⋯).IsIntegral<GOAL>⊥.jacobson = ⊥
<VAR>R : Type u_5<VAR>CommRing R<VAR>IsDomain R<VAR>hR : Ideal.IsJacobson R<VAR>P : Ideal (Polynomial R)<VAR>P.IsPrime<VAR>hP : ∀ (x : R), Polynomial.C x ∈ P → x = 0<GOAL>P.jacobson = P
<VAR>R : Type u_1<VAR>CommRing R<VAR>hR : Ideal.IsJacobson R<GOAL>Ideal.IsJacobson (Polynomial R)
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Ideal.IsJacobson (Polynomial R) ↔ Ideal.IsJacobson R
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ideal.IsJacobson R<VAR>P : Ideal (Polynomial R)<VAR>hP : P.IsMaximal<VAR>Nontrivial R<VAR>hP' : ∀ (x : R), Polynomial.C x ∈ P → x = 0<GOAL>(Ideal.comap Polynomial.C P).IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Ideal (Polynomial R)<VAR>hP : P.IsMaximal<VAR>Nontrivial R<VAR>hR : Ideal.IsJacobson R<VAR>hP' : ∀ (x : R), Polynomial.C x ∈ P → x = 0<GOAL>((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegral
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ideal.IsJacobson R<VAR>P : Ideal (Polynomial R)<VAR>hP : P.IsMaximal<GOAL>((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegral
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ideal.IsJacobson R<VAR>P : Ideal (Polynomial R)<VAR>hP : P.IsMaximal<GOAL>(Ideal.comap Polynomial.C P).IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ideal.IsJacobson R<VAR>S : Type u_2<VAR>Field S<VAR>f : Polynomial R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>(f.comp Polynomial.C).IsIntegral
<VAR>R : Type u<VAR>CommRing R<VAR>H : Ideal.IsJacobson R<VAR>n : ℕ<GOAL>Ideal.IsJacobson (MvPolynomial (Fin n) R)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Ideal.IsJacobson S<VAR>Algebra R S<VAR>Algebra R T<VAR>IH : ∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral<VAR>v : Polynomial S ≃ₐ[R] T<VAR>P : Ideal T<VAR>hP : P.IsMaximal<GOAL>(algebraMap R (T ⧸ P)).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>Ideal.IsJacobson R<VAR>P : Ideal (MvPolynomial (Fin n) R)<VAR>hP : P.IsMaximal<GOAL>(algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>Ideal.IsJacobson R<VAR>P : Ideal (MvPolynomial (Fin n) R)<VAR>hP : P.IsMaximal<GOAL>((Ideal.Quotient.mk P).comp MvPolynomial.C).IsIntegral
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ideal.IsJacobson R<VAR>σ : Type u_2<VAR>Finite σ<VAR>S : Type u_3<VAR>Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>(f.comp MvPolynomial.C).IsIntegral
<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>self : IsLocalization M S<VAR>x y : R<GOAL>(algebraMap R S) x = (algebraMap R S) 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<GOAL>IsLocalization M S ↔ (∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧ (∀ (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧ ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) 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>self : IsLocalization M S<VAR>y : ↥M<GOAL>IsUnit ((algebraMap R S) ↑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>self : IsLocalization M S<VAR>z : S<GOAL>∃ 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>y : ↥M<GOAL>IsUnit ((algebraMap R S) ↑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>IsLocalization M S<VAR>z : S<GOAL>∃ 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>x y : R<GOAL>(algebraMap R S) x = (algebraMap R S) 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>IsLocalization M S<VAR>N : Submonoid R<VAR>h₁ : M ≤ N<VAR>h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)<GOAL>IsLocalization N S
<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>a : R<GOAL>(↑(IsLocalization.toLocalizationWithZeroMap M S).toMonoidHom).toFun a = (algebraMap R S) a
<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<GOAL>(IsLocalization.toLocalizationMap M S).toMap = ↑↑(algebraMap R S)
<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>x : R<GOAL>(IsLocalization.toLocalizationMap M S).toMap x = (algebraMap R S) x
<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>z w : S<GOAL>∃ z' w' d, z * (algebraMap R S) ↑d = (algebraMap R S) z' ∧ w * (algebraMap R S) ↑d = (algebraMap R S) w'
<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<GOAL>(IsLocalization.toLocalizationMap M S).sec = IsLocalization.sec M
<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>z : S<GOAL>z * (algebraMap R S) ↑(IsLocalization.sec M z).2 = (algebraMap R S) (IsLocalization.sec M z).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>z : S<GOAL>(algebraMap R S) (IsLocalization.sec M z).1 = (algebraMap R S) ↑(IsLocalization.sec M z).2 * z
<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>h : 0 ∈ M<GOAL>Subsingleton S
<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>x y : R<VAR>c : ↥M<VAR>h : (algebraMap R S) (↑c * x) = (algebraMap R S) (↑c * y)<GOAL>(algebraMap R S) x = (algebraMap R S) 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>IsLocalization M S<VAR>x y : R<VAR>c : ↥M<VAR>h : (algebraMap R S) (x * ↑c) = (algebraMap R S) (y * ↑c)<GOAL>(algebraMap R S) x = (algebraMap R S) 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>IsLocalization M S<VAR>z : S<VAR>x : R<VAR>y : ↥M<VAR>h : z * (algebraMap R S) ↑y = (algebraMap R S) x<VAR>hx : x = 0<GOAL>z = 0
<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>r : R<GOAL>(algebraMap R S) r = 0 ↔ ∃ m, ↑m * r = 0
<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>z : S<GOAL>IsLocalization.mk' S (IsLocalization.sec M z).1 (IsLocalization.sec M z).2 = z
<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>x₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>IsLocalization.mk' S (x₁ * x₂) (y₁ * y₂) = IsLocalization.mk' S x₁ y₁ * IsLocalization.mk' S x₂ 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>IsLocalization M S<VAR>x : R<GOAL>IsLocalization.mk' S x 1 = (algebraMap R S) x
<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>x : R<VAR>y : ↥M<GOAL>IsLocalization.mk' S x y * (algebraMap R S) ↑y = (algebraMap R S) x
<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>x : R<VAR>y : ↥M<GOAL>(algebraMap R S) ↑y * IsLocalization.mk' S x y = (algebraMap R S) x
<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>x y : R<VAR>hy : y ∈ M<GOAL>IsLocalization.mk' S x ⟨y, hy⟩ * (algebraMap R S) y = (algebraMap R S) x
<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>x y : R<VAR>hy : y ∈ M<GOAL>(algebraMap R S) y * IsLocalization.mk' S x ⟨y, hy⟩ = (algebraMap R S) x
<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>x : R<VAR>y : ↥M<VAR>z : S<GOAL>z = IsLocalization.mk' S x y ↔ z * (algebraMap R S) ↑y = (algebraMap R S) x
<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>x : R<VAR>y : ↥M<VAR>z : S<GOAL>IsLocalization.mk' S x y = z ↔ (algebraMap R S) x = z * (algebraMap R S) ↑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>IsLocalization M S<VAR>x : R<VAR>y : ↥M<VAR>z₁ z₂ : S<GOAL>IsLocalization.mk' S x y + z₁ = z₂ ↔ (algebraMap R S) x + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑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>IsLocalization M S<VAR>x : R<VAR>y : ↥M<VAR>n : ℕ<GOAL>IsLocalization.mk' S (x ^ n) (y ^ n) = IsLocalization.mk' S x y ^ n
<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>z : S<GOAL>∃ x y, IsLocalization.mk' S x y = z
<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>x₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ (algebraMap R S) (↑y₂ * x₁) = (algebraMap R S) (↑y₁ * x₂)
<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>x₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ (algebraMap R S) (x₁ * ↑y₂) = (algebraMap R S) (x₂ * ↑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>IsLocalization M S<VAR>x : R<VAR>y : ↥M<VAR>I : Ideal S<GOAL>IsLocalization.mk' S x y ∈ I ↔ (algebraMap R 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>a₁ b₁ : R<VAR>a₂ b₂ : ↥M<GOAL>IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂ ↔ ∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)
<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>x : R<VAR>s : ↥M<GOAL>IsLocalization.mk' S x s = 0 ↔ ∃ m, ↑m * x = 0
<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>s : ↥M<GOAL>IsLocalization.mk' S 0 s = 0
<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>x : R<VAR>y : ↥M<VAR>hxy : IsLocalization.mk' S x y ≠ 0<GOAL>x ≠ 0
<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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>Algebra R P<VAR>IsLocalization M P<VAR>x y : R<GOAL>(algebraMap R S) x = (algebraMap R S) y ↔ (algebraMap R P) x = (algebraMap R P) 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>Algebra R P<VAR>IsLocalization M P<VAR>x₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>IsLocalization.mk' S x₁ y₁ = IsLocalization.mk' S x₂ y₂ ↔ IsLocalization.mk' P x₁ y₁ = IsLocalization.mk' P x₂ 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>IsLocalization M S<VAR>a₁ b₁ : R<VAR>a₂ b₂ : ↥M<VAR>H : ↑a₂ * b₁ = ↑b₂ * a₁<GOAL>IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂
<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>a₁ b₁ : R<VAR>a₂ b₂ : ↥M<VAR>H : b₁ * ↑a₂ = a₁ * ↑b₂<GOAL>IsLocalization.mk' S a₁ a₂ = IsLocalization.mk' S b₁ b₂
<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>a : R<VAR>b c : ↥M<GOAL>IsLocalization.mk' S (a * ↑c) (b * c) = IsLocalization.mk' S a b
<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>x : R<VAR>hx : x ∈ M<GOAL>IsLocalization.mk' S x ⟨x, hx⟩ = 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>x : ↥M<GOAL>IsLocalization.mk' S (↑x) 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>x y : R<VAR>z : ↥M<GOAL>(algebraMap R S) x * IsLocalization.mk' S y z = IsLocalization.mk' S (x * y) z
<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>x : R<VAR>y : ↥M<GOAL>IsLocalization.mk' S x y = (algebraMap R S) x * IsLocalization.mk' S 1 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>IsLocalization M S<VAR>x : R<VAR>y : ↥M<GOAL>IsLocalization.mk' S (↑y * x) y = (algebraMap R S) x
<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>x : R<VAR>y : ↥M<GOAL>IsLocalization.mk' S (x * ↑y) y = (algebraMap R S) x
<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>x y : ↥M<GOAL>IsLocalization.mk' S (↑x) y * IsLocalization.mk' S (↑y) 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>x : R<VAR>y : ↥M<VAR>h : x ∈ M<GOAL>IsLocalization.mk' S x y * IsLocalization.mk' S ↑y ⟨x, h⟩ = 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>x y : R<VAR>m : ↥M<GOAL>x • IsLocalization.mk' S y m = IsLocalization.mk' S (x * y) m