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>IsLocalization M S<VAR>x : R<VAR>m : ↥M<GOAL>x • IsLocalization.mk' S 1 m = IsLocalization.mk' S x 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>m : ↥M<VAR>r : R<GOAL>↑m • IsLocalization.mk' S r m = (algebraMap R S) r
<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 1 s) = (algebraMap R S) ↑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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>j : S →+* P<VAR>y : ↥M<GOAL>IsUnit ((j.comp (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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>x y : R<VAR>h : (algebraMap R S) x = (algebraMap R S) y<GOAL>g x = g 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₁ x₂ : R<VAR>y₁ y₂ : ↥M<GOAL>IsLocalization.mk' S (x₁ * ↑y₂ + x₂ * ↑y₁) (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>P : Type u_3<VAR>CommSemiring P<VAR>g : R →+* P<VAR>h : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>y : ↥M<VAR>w z₁ z₂ : P<GOAL>w * ↑((IsUnit.liftRight ((↑g).restrict M) h) y)⁻¹ + z₁ = z₂ ↔ w + g ↑y * z₁ = g ↑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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>z : S<VAR>w w' v : P<GOAL>((IsLocalization.toLocalizationWithZeroMap M S).lift g.toMonoidWithZeroHom hg) z * w + w' = v ↔ g ((IsLocalization.toLocalizationMap M S).sec z).1 * w + g ↑((IsLocalization.toLocalizationMap M S).sec z).2 * w' = g ↑((IsLocalization.toLocalizationMap M S).sec z).2 * v
<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>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>x : R<VAR>y : ↥M<GOAL>(IsLocalization.lift hg) (IsLocalization.mk' S x y) = g x * ↑((IsUnit.liftRight ((↑g).restrict M) hg) 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>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>x : R<VAR>v : P<VAR>y : ↥M<GOAL>(IsLocalization.lift hg) (IsLocalization.mk' S x y) = v ↔ g x = g ↑y * v
<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>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>x : R<GOAL>(IsLocalization.lift hg) ((algebraMap R S) x) = g 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>x y : R × ↥M<GOAL>(IsLocalization.lift hg) (IsLocalization.mk' S x.1 x.2) = (IsLocalization.lift hg) (IsLocalization.mk' S y.1 y.2) ↔ g (x.1 * ↑y.2) = g (y.1 * ↑x.2)
<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>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<GOAL>(IsLocalization.lift hg).comp (algebraMap R S) = g
<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>j : S →+* P<GOAL>IsLocalization.lift ⋯ = 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>j k : S →* P<VAR>h : j.comp ↑(algebraMap R S) = k.comp ↑(algebraMap R S)<GOAL>j = k
<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>j k : S →+* P<VAR>h : j.comp (algebraMap R S) = k.comp (algebraMap R S)<GOAL>j = k
<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<GOAL>Subsingleton (S →ₐ[R] P)
<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>j k : S → P<VAR>hj1 : j 1 = 1<VAR>hk1 : k 1 = 1<VAR>hjm : ∀ (a b : S), j (a * b) = j a * j b<VAR>hkm : ∀ (a b : S), k (a * b) = k a * k b<VAR>h : ∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)<GOAL>j = k
<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>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>j : S →+* P<VAR>hj : ∀ (x : R), j ((algebraMap R S) x) = g x<GOAL>IsLocalization.lift hg = 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>x : S<GOAL>(IsLocalization.lift ⋯) x = 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<GOAL>Function.Surjective ⇑(IsLocalization.lift hg) ↔ ∀ (v : P), ∃ x, v * g ↑x.2 = g 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<GOAL>Function.Injective ⇑(IsLocalization.lift hg) ↔ ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ g x = g 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>g : R →+* P<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>x : R<GOAL>(IsLocalization.map Q g hy) ((algebraMap R S) x) = (algebraMap P Q) (g 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>Algebra P Q<VAR>IsLocalization T Q<GOAL>(IsLocalization.map Q g hy).comp (algebraMap R S) = (algebraMap P Q).comp g
<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>g : R →+* P<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>x : R<VAR>y : ↥M<GOAL>(IsLocalization.map Q g hy) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (g x) ⟨g ↑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>Q : Type u_5<VAR>CommSemiring Q<VAR>Algebra R Q<VAR>IsLocalization M Q<VAR>x : R<VAR>y : ↥M<GOAL>(IsLocalization.map Q (RingHom.id R) ⋯) (IsLocalization.mk' S x y) = IsLocalization.mk' Q 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>z : S<VAR>h : M ≤ Submonoid.comap (RingHom.id R) M := ⋯<GOAL>(IsLocalization.map S (RingHom.id R) h) z = 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>j : S →+* Q<VAR>hj : ∀ (x : R), j ((algebraMap R S) x) = (algebraMap P Q) (g x)<GOAL>IsLocalization.map Q g hy = 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>A : Type u_5<VAR>CommSemiring A<VAR>U : Submonoid A<VAR>W : Type u_6<VAR>CommSemiring W<VAR>Algebra A W<VAR>IsLocalization U W<VAR>l : P →+* A<VAR>hl : T ≤ Submonoid.comap l U<GOAL>(IsLocalization.map W l hl).comp (IsLocalization.map Q g hy) = IsLocalization.map W (l.comp g) ⋯
<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>g : R →+* P<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>A : Type u_5<VAR>CommSemiring A<VAR>U : Submonoid A<VAR>W : Type u_6<VAR>CommSemiring W<VAR>Algebra A W<VAR>IsLocalization U W<VAR>l : P →+* A<VAR>hl : T ≤ Submonoid.comap l U<VAR>x : S<GOAL>(IsLocalization.map W l hl) ((IsLocalization.map Q g hy) x) = (IsLocalization.map W (l.comp g) ⋯) 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>g : R →+* P<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>hy : M ≤ Submonoid.comap g T<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>x : S<VAR>z : R<GOAL>(IsLocalization.map Q g hy) (z • x) = g z • (IsLocalization.map Q g hy) 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<VAR>a : S<GOAL>(IsLocalization.ringEquivOfRingEquiv S Q h H) a = (IsLocalization.map Q ↑h ⋯) 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>h : R ≃+* P<VAR>H : Submonoid.map h.toMonoidHom M = T<VAR>a : Q<GOAL>(IsLocalization.ringEquivOfRingEquiv S Q h H).symm a = (IsLocalization.map S ↑h.symm ⋯) 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>j : R ≃+* P<VAR>H : Submonoid.map j.toMonoidHom M = T<GOAL>↑(IsLocalization.ringEquivOfRingEquiv S Q j H) = IsLocalization.map Q ↑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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>j : R ≃+* P<VAR>H : Submonoid.map j.toMonoidHom M = T<VAR>x : R<GOAL>(IsLocalization.ringEquivOfRingEquiv S Q j H) ((algebraMap R S) x) = (algebraMap P Q) (j 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>P : Type u_3<VAR>CommSemiring P<VAR>IsLocalization M S<VAR>T : Submonoid P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra P Q<VAR>IsLocalization T Q<VAR>j : R ≃+* P<VAR>H : Submonoid.map j.toMonoidHom M = T<VAR>x : R<VAR>y : ↥M<GOAL>(IsLocalization.ringEquivOfRingEquiv S Q j H) (IsLocalization.mk' S x y) = IsLocalization.mk' Q (j x) ⟨j ↑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>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra R Q<VAR>IsLocalization M Q<VAR>a : S<GOAL>(IsLocalization.algEquiv M S Q) a = (IsLocalization.map Q (RingHom.id R) ⋯) 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<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra R Q<VAR>IsLocalization M Q<VAR>a : Q<GOAL>(IsLocalization.algEquiv M S Q).symm a = (IsLocalization.map S (RingHom.id R) ⋯) 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<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra R Q<VAR>IsLocalization M Q<VAR>x : R<VAR>y : ↥M<GOAL>(IsLocalization.algEquiv M S Q) (IsLocalization.mk' S x y) = IsLocalization.mk' Q 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>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra R Q<VAR>IsLocalization M Q<VAR>x : R<VAR>y : ↥M<GOAL>(IsLocalization.algEquiv M S Q).symm (IsLocalization.mk' Q 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>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra R Q<VAR>IsLocalization M Q<VAR>f : S →+* Q<VAR>hf : f.comp (algebraMap R S) = algebraMap R Q<GOAL>Function.Bijective ⇑f
<VAR>R : Type u_4<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>hS : S ≤ IsUnit.submonoid R<GOAL>IsLocalization S R
<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>g : R →+* P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra P Q<VAR>h : Function.Injective ⇑g<VAR>IsLocalization (Submonoid.map g M) Q<GOAL>Function.Injective ⇑(IsLocalization.map Q g ⋯)
<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>g : R →+* P<VAR>Q : Type u_4<VAR>CommSemiring Q<VAR>Algebra P Q<VAR>h : Function.Surjective ⇑g<VAR>IsLocalization (Submonoid.map g M) Q<GOAL>Function.Surjective ⇑(IsLocalization.map Q g ⋯)
<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>Algebra R P<VAR>IsLocalization M S<VAR>h : S ≃ₐ[R] P<GOAL>IsLocalization M P
<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>Algebra R P<VAR>h : S ≃ₐ[R] P<GOAL>IsLocalization M S ↔ IsLocalization M P
<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>h : S ≃+* P<GOAL>IsLocalization M S ↔ IsLocalization M P
<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>h : R ≃+* P<GOAL>IsLocalization (Submonoid.map h.toMonoidHom M) 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>P : Type u_3<VAR>CommSemiring P<VAR>h : R ≃+* P<GOAL>IsLocalization M S ↔ IsLocalization (Submonoid.map h.toMonoidHom M) 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<GOAL>nonZeroDivisors R ≤ Submonoid.comap (algebraMap R S) (nonZeroDivisors 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<GOAL>Submonoid.map (algebraMap R S) (nonZeroDivisors R) ≤ nonZeroDivisors S
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>a : R<VAR>b : ↥M<VAR>c : R<VAR>d : ↥M<GOAL>Localization.mk a b + Localization.mk c d = Localization.mk (↑b * c + ↑d * a) (b * d)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>a : R<VAR>b : ↥M<VAR>c : R<GOAL>Localization.mk a b + Localization.mk c b = Localization.mk (a + c) b
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>b : ↥M<VAR>a : R<GOAL>(Localization.mkAddMonoidHom b) a = Localization.mk a b
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>ι : Type u_4<VAR>f : ι → R<VAR>s : Finset ι<VAR>b : ↥M<GOAL>Localization.mk (∑ i ∈ s, f i) b = ∑ i ∈ s, Localization.mk (f i) b
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>l : List R<VAR>b : ↥M<GOAL>Localization.mk l.sum b = (List.map (fun a => Localization.mk a b) l).sum
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>l : Multiset R<VAR>b : ↥M<GOAL>Localization.mk l.sum b = (Multiset.map (fun a => Localization.mk a b) l).sum
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<GOAL>IsLocalization.toLocalizationMap M (Localization M) = Localization.monoidOf M
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>x : R<GOAL>(Localization.monoidOf M).toMap x = (algebraMap R (Localization M)) x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>x : R<GOAL>Localization.mk x 1 = (algebraMap R (Localization M)) x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>x : R<VAR>y : ↥M<GOAL>Localization.mk x y = IsLocalization.mk' (Localization M) x y
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<GOAL>Localization.mk = IsLocalization.mk' (Localization M)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>A : Type u_4<VAR>CommSemiring A<VAR>Algebra A R<VAR>m : A<GOAL>Localization.mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>m : ℕ<GOAL>Localization.mk (↑m) 1 = ↑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>a : Localization M<GOAL>(Localization.algEquiv M S) a = (IsLocalization.map S (RingHom.id R) ⋯) 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<VAR>a : S<GOAL>(Localization.algEquiv M S).symm a = (IsLocalization.map (Localization M) (RingHom.id R) ⋯) 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<VAR>x : R<VAR>y : ↥M<GOAL>(Localization.algEquiv M S) (IsLocalization.mk' (Localization M) 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<VAR>y : ↥M<GOAL>(Localization.algEquiv M S).symm (IsLocalization.mk' S x y) = IsLocalization.mk' (Localization M) 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<GOAL>(Localization.algEquiv M S) (Localization.mk 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<VAR>y : ↥M<GOAL>(Localization.algEquiv M S).symm (IsLocalization.mk' S x y) = Localization.mk 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<GOAL>↑(Localization.algEquiv M S) = IsLocalization.map S (RingHom.id R) ⋯
<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>↑(Localization.algEquiv M S).symm = IsLocalization.map (Localization M) (RingHom.id R) ⋯
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>a : R<VAR>b : ↥M<GOAL>-Localization.mk a b = Localization.mk (-a) b
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>a c : R<VAR>b d : ↥M<GOAL>Localization.mk a b - Localization.mk c d = Localization.mk (↑d * a - ↑b * c) (b * d)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>m : ℤ<GOAL>Localization.mk (↑m) 1 = ↑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 : R<VAR>hM : M ≤ nonZeroDivisors R<GOAL>(algebraMap R S) x = 0 ↔ x = 0
<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>hM : M ≤ nonZeroDivisors R<GOAL>Function.Injective ⇑(algebraMap R 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>Nontrivial R<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : R<VAR>hx : x ∈ nonZeroDivisors R<GOAL>(algebraMap R S) x ≠ 0
<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>Nontrivial R<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : S<GOAL>↑(IsLocalization.sec M x).2 ≠ 0
<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>Nontrivial R<VAR>NoZeroDivisors S<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : S<VAR>hx : x ≠ 0<GOAL>(IsLocalization.sec M x).1 ≠ 0
<VAR>S : Type u_2<VAR>CommRing S<VAR>A : Type u_6<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra A S<VAR>M : Submonoid A<VAR>IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<GOAL>NoZeroDivisors S
<VAR>S : Type u_2<VAR>CommRing S<VAR>A : Type u_6<VAR>CommRing A<VAR>IsDomain A<VAR>Algebra A S<VAR>M : Submonoid A<VAR>IsLocalization M S<VAR>hM : M ≤ nonZeroDivisors A<GOAL>IsDomain S
<VAR>A : Type u_6<VAR>CommRing A<VAR>IsDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ nonZeroDivisors A<GOAL>IsDomain (Localization M)
<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>CommRing R<VAR>CommRing Rₘ<VAR>M : Submonoid R<VAR>hM : 0 ∉ M<VAR>hR : IsField R<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<GOAL>Function.Bijective ⇑(algebraMap R Rₘ)
<VAR>K : Type u_4<VAR>Kₘ : Type u_5<VAR>Field K<VAR>CommRing Kₘ<VAR>M : Submonoid K<VAR>hM : 0 ∉ M<VAR>Algebra K Kₘ<VAR>IsLocalization M Kₘ<GOAL>Function.Bijective ⇑(algebraMap K Kₘ)
<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>Sₘ : Type u_5<VAR>CommRing Sₘ<VAR>Algebra S Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R S Sₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>y : ↥M<GOAL>IsUnit ((algebraMap R Sₘ) ↑y)
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>i : 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>x : R<VAR>y : ↥M<GOAL>(algebraMap Rₘ Sₘ) (IsLocalization.mk' Rₘ x y) = IsLocalization.mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩
<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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<GOAL>algebraMap Rₘ Sₘ = IsLocalization.map Sₘ (algebraMap R 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>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>CommRing Rₘ<VAR>CommRing Sₘ<VAR>Algebra R Rₘ<VAR>IsLocalization M Rₘ<VAR>Algebra S Sₘ<VAR>i : 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>x : Rₘ<GOAL>(algebraMap Rₘ Sₘ) x = (IsLocalization.map Sₘ (algebraMap R S) ⋯) x