ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>I : Ideal S<VAR>hI : Nat.Prime (Ideal.absNorm I)<GOAL>Ideal.span {↑(Ideal.absNorm I)} = Ideal.comap (algebraMap ℤ S) I
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>CharZero S<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>{I | Ideal.absNorm I = n}.Finite
<VAR>S : Type u_1<VAR>CommRing S<VAR>IsDomain S<VAR>Nontrivial S<VAR>IsDedekindDomain S<VAR>Module.Free ℤ S<VAR>Module.Finite ℤ S<VAR>x : S<VAR>hx : Prime ((Algebra.norm ℤ) x)<VAR>y : ℤ<GOAL>(Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Nontrivial S<VAR>Module.Free R S<VAR>Module.Finite R S<GOAL>Ideal.spanNorm R ⊥ = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>I : Ideal S<GOAL>Ideal.spanNorm R I = ⊥ ↔ I = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal S<VAR>x : S<VAR>hx : x ∈ I<GOAL>(Algebra.norm R) x ∈ Ideal.spanNorm R I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>r : S<GOAL>Ideal.spanNorm R (Ideal.span {r}) = Ideal.span {(Algebra.norm R) r}
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<GOAL>Ideal.spanNorm R ⊤ = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal S<VAR>T : Type u_3<VAR>CommRing T<VAR>f : R →+* T<GOAL>Ideal.map f (Ideal.spanNorm R I) = Ideal.span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I J : Ideal S<VAR>h : I ≤ J<GOAL>Ideal.spanNorm R I ≤ Ideal.spanNorm R J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>M : Submonoid R<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>Algebra Rₘ Sₘ<VAR>Algebra R Sₘ<VAR>IsScalarTower R Rₘ Sₘ<VAR>IsScalarTower R S Sₘ<VAR>IsLocalization M Rₘ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<GOAL>Ideal.spanNorm Rₘ (Ideal.map (algebraMap S Sₘ) I) = Ideal.map (algebraMap R Rₘ) (Ideal.spanNorm R I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I J : Ideal S<GOAL>Ideal.spanNorm R I * Ideal.spanNorm R J ≤ Ideal.spanNorm R (I * J)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤<VAR>I J : Ideal S<GOAL>Ideal.spanNorm R (I * J) = Ideal.spanNorm R I * Ideal.spanNorm R J
<VAR>S : Type u_2<VAR>CommRing S<VAR>K : Type u_3<VAR>Field K<VAR>Algebra K S<VAR>IsDomain S<VAR>Module.Finite K S<VAR>I J : Ideal S<GOAL>Ideal.spanNorm K (I * J) = Ideal.spanNorm K I * Ideal.spanNorm K J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>I J : Ideal S<GOAL>Ideal.spanNorm R (I * J) = Ideal.spanNorm R I * Ideal.spanNorm R J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>I : Ideal S<GOAL>(Ideal.relNorm R) I = Ideal.span (⇑(Algebra.norm R) '' ↑I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>I : Ideal S<GOAL>Ideal.spanNorm R I = (Ideal.relNorm R) I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<GOAL>(Ideal.relNorm R) ⊥ = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<GOAL>(Ideal.relNorm R) ⊤ = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>I : Ideal S<GOAL>(Ideal.relNorm R) I = ⊥ ↔ I = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>I : Ideal S<VAR>x : S<VAR>hx : x ∈ I<GOAL>(Algebra.norm R) x ∈ (Ideal.relNorm R) I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>r : S<GOAL>(Ideal.relNorm R) (Ideal.span {r}) = Ideal.span {(Algebra.norm R) r}
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>I : Ideal S<VAR>T : Type u_3<VAR>CommRing T<VAR>f : R →+* T<GOAL>Ideal.map f ((Ideal.relNorm R) I) = Ideal.span (⇑f ∘ ⇑(Algebra.norm R) '' ↑I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>IsDedekindDomain R<VAR>IsDedekindDomain S<VAR>Module.Finite R S<VAR>Module.Free R S<VAR>I J : Ideal S<VAR>h : I ≤ J<GOAL>(Ideal.relNorm R) I ≤ (Ideal.relNorm R) J
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>Ring R<VAR>Ring S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module S N<VAR>SMulCommClass R S N<VAR>StrongRankCondition R<VAR>StrongRankCondition S<VAR>Module.Free S N<GOAL>Module.rank S (M →ₗ[R] N) = Cardinal.lift.{w, v} (Module.rank R M) * Cardinal.lift.{v, w} (Module.rank S N)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>N : Type w<VAR>Ring R<VAR>Ring S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>AddCommGroup N<VAR>Module R N<VAR>Module S N<VAR>SMulCommClass R S N<VAR>StrongRankCondition R<VAR>StrongRankCondition S<VAR>Module.Free S N<GOAL>FiniteDimensional.finrank S (M →ₗ[R] N) = FiniteDimensional.finrank R M * FiniteDimensional.finrank S N
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>Ring R<VAR>Ring S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>StrongRankCondition R<VAR>StrongRankCondition S<VAR>Module R S<VAR>SMulCommClass R S S<GOAL>Module.rank S (M →ₗ[R] S) = Cardinal.lift.{u', v} (Module.rank R M)
<VAR>R : Type u<VAR>S : Type u'<VAR>M : Type v<VAR>Ring R<VAR>Ring S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Free R M<VAR>Module.Finite R M<VAR>StrongRankCondition R<VAR>StrongRankCondition S<VAR>Module R S<VAR>SMulCommClass R S S<GOAL>FiniteDimensional.finrank S (M →ₗ[R] S) = FiniteDimensional.finrank R M
<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>CommRing K<VAR>Ring M<VAR>Algebra K M<VAR>Module.Free K M<VAR>Module.Finite K M<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<GOAL>Cardinal.mk (M →ₐ[K] L) ≤ Cardinal.lift.{v, u_2} (Module.rank K M)
<VAR>K : Type u_1<VAR>M : Type u_2<VAR>L : Type v<VAR>CommRing K<VAR>Ring M<VAR>Algebra K M<VAR>Module.Free K M<VAR>Module.Finite K M<VAR>CommRing L<VAR>IsDomain L<VAR>Algebra K L<GOAL>Nat.card (M →ₐ[K] L) ≤ FiniteDimensional.finrank K M
<VAR>K m n : Type u<VAR>CommRing K<VAR>Fintype n<VAR>DecidableEq n<VAR>w : m → K<VAR>v : n → K<GOAL>(Matrix.toLin' (Matrix.vecMulVec w v)).rank ≤ 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>β : OreLocalization S X → Prop<VAR>c : ∀ (r : X) (s : ↥S), β (r /ₒ s)<VAR>q : OreLocalization S X<GOAL>β q
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>β : AddOreLocalization S X → Prop<VAR>c : ∀ (r : X) (s : ↥S), β (r -ₒ s)<VAR>q : AddOreLocalization S X<GOAL>β q
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r₁ r₂ : X<VAR>s₁ s₂ : ↥S<GOAL>r₁ -ₒ s₁ = r₂ -ₒ s₂ ↔ ∃ u v, u +ᵥ r₂ = v +ᵥ r₁ ∧ ↑u + ↑s₂ = v + ↑s₁
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r₁ r₂ : X<VAR>s₁ s₂ : ↥S<GOAL>r₁ /ₒ s₁ = r₂ /ₒ s₂ ↔ ∃ u v, u • r₂ = v • r₁ ∧ ↑u * ↑s₂ = v * ↑s₁
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r : X<VAR>s : ↥S<VAR>t : R<VAR>hst : t * ↑s ∈ S<GOAL>r /ₒ s = t • r /ₒ ⟨t * ↑s, hst⟩
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r : X<VAR>s : ↥S<VAR>t : R<VAR>hst : t + ↑s ∈ S<GOAL>r -ₒ s = t +ᵥ r -ₒ ⟨t + ↑s, hst⟩
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r : X<VAR>s s' : ↥S<GOAL>r /ₒ s = s' • r /ₒ (s' * s)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r : X<VAR>s s' : ↥S<GOAL>r -ₒ s = s' +ᵥ r -ₒ (s' + s)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r r' r₁ r₂ : R<VAR>s t : ↥S<VAR>h : ↑t * r = ↑t * r'<GOAL>r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r r' r₁ r₂ : R<VAR>s t : ↥S<VAR>h : ↑t + r = ↑t + r'<GOAL>r₁ + r + r₂ -ₒ s = r₁ + r' + r₂ -ₒ s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_3<VAR>MulAction R X<VAR>C : Sort u_2<VAR>P : X → ↥S → C<VAR>hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩<VAR>r : X<VAR>s : ↥S<GOAL>OreLocalization.liftExpand P hP (r /ₒ s) = P r s
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_3<VAR>AddAction R X<VAR>C : Sort u_2<VAR>P : X → ↥S → C<VAR>hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t + ↑s ∈ S), P r s = P (t +ᵥ r) ⟨t + ↑s, ht⟩<VAR>r : X<VAR>s : ↥S<GOAL>AddOreLocalization.liftExpand P hP (r -ₒ s) = P r s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_3<VAR>MulAction R X<VAR>C : Sort u_2<VAR>P : X → ↥S → X → ↥S → C<VAR>hP : ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S), P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<GOAL>OreLocalization.lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_3<VAR>AddAction R X<VAR>C : Sort u_2<VAR>P : X → ↥S → X → ↥S → C<VAR>hP : ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ + ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ + ↑s₂ ∈ S), P r₁ s₁ r₂ s₂ = P (t₁ +ᵥ r₁) ⟨t₁ + ↑s₁, ht₁⟩ (t₂ +ᵥ r₂) ⟨t₂ + ↑s₂, ht₂⟩<VAR>r₁ : X<VAR>s₁ : ↥S<VAR>r₂ : X<VAR>s₂ : ↥S<GOAL>AddOreLocalization.lift₂Expand P hP (r₁ -ₒ s₁) (r₂ -ₒ s₂) = P r₁ s₁ r₂ s₂
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u + r₁ = v + ↑s₂<GOAL>OreLocalization.vadd' r₁ s₁ r₂ s₂ = v +ᵥ r₂ -ₒ (u + s₁)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ u : ↥S<VAR>v : R<VAR>huv : ↑u * r₁ = v * ↑s₂<GOAL>OreLocalization.smul' r₁ s₁ r₂ s₂ = v • r₂ /ₒ (u * s₁)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ : ↥S<GOAL>(r₁ /ₒ s₁) • (r₂ /ₒ s₂) = OreLocalization.oreNum r₁ s₂ • r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ : ↥S<GOAL>r₁ -ₒ s₁ +ᵥ (r₂ -ₒ s₂) = AddOreLocalization.oreMin r₁ s₂ +ᵥ r₂ -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<GOAL>r₁ -ₒ s₁ + (r₂ -ₒ s₂) = AddOreLocalization.oreMin r₁ s₂ + r₂ -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<GOAL>r₁ /ₒ s₁ * (r₂ /ₒ s₂) = OreLocalization.oreNum r₁ s₂ * r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ : ↥S<VAR>r' : R<VAR>s' : ↥S<VAR>huv : ↑s' * r₁ = r' * ↑s₂<GOAL>(r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s₁ s₂ : ↥S<VAR>r' : R<VAR>s' : ↥S<VAR>huv : ↑s' + r₁ = r' + ↑s₂<GOAL>r₁ -ₒ s₁ +ᵥ (r₂ -ₒ s₂) = r' +ᵥ r₂ -ₒ (s' + s₁)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<VAR>r' : R<VAR>s' : ↥S<VAR>huv : ↑s' + r₁ = r' + ↑s₂<GOAL>r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r' + r₂ -ₒ (s' + s₁)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r₁ r₂ : R<VAR>s₁ s₂ : ↥S<VAR>r' : R<VAR>s' : ↥S<VAR>huv : ↑s' * r₁ = r' * ↑s₂<GOAL>r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<GOAL>0 = 0 -ₒ 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<GOAL>1 = 1 /ₒ 1
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r : R<VAR>hr : r ∈ S<GOAL>r -ₒ ⟨r, hr⟩ = 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r : R<VAR>hr : r ∈ S<GOAL>r /ₒ ⟨r, hr⟩ = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>s : ↥S<GOAL>↑s /ₒ s = 1
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>s : ↥S<GOAL>↑s -ₒ s = 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>x : OreLocalization S X<GOAL>1 • x = x
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>x : AddOreLocalization S X<GOAL>0 +ᵥ x = x
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>x : OreLocalization S R<GOAL>1 * x = x
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>x : AddOreLocalization S R<GOAL>0 + x = x
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>x : OreLocalization S R<GOAL>x * 1 = x
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>x : AddOreLocalization S R<GOAL>x + 0 = x
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>x y : AddOreLocalization S R<VAR>z : AddOreLocalization S X<GOAL>x + y +ᵥ z = x +ᵥ (y +ᵥ z)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>x y : OreLocalization S R<VAR>z : OreLocalization S X<GOAL>(x * y) • z = x • y • z
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>x y z : OreLocalization S R<GOAL>x * y * z = x * (y * z)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>x y z : AddOreLocalization S R<GOAL>x + y + z = x + (y + z)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>s s' : ↥S<GOAL>↑s -ₒ s' + (↑s' -ₒ s) = 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>s s' : ↥S<GOAL>↑s /ₒ s' * (↑s' /ₒ s) = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r : X<VAR>s t : ↥S<GOAL>(1 /ₒ t) • (r /ₒ s) = r /ₒ (s * t)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r : X<VAR>s t : ↥S<GOAL>0 -ₒ t +ᵥ (r -ₒ s) = r -ₒ (s + t)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r : R<VAR>s t : ↥S<GOAL>1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r : R<VAR>s t : ↥S<GOAL>0 -ₒ t + (r -ₒ s) = r -ₒ (s + t)
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r : X<VAR>s t : ↥S<GOAL>(↑s /ₒ t) • (r /ₒ s) = r /ₒ t
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r : X<VAR>s t : ↥S<GOAL>↑s -ₒ t +ᵥ (r -ₒ s) = r -ₒ t
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r : R<VAR>s t : ↥S<GOAL>↑s /ₒ t * (r /ₒ s) = r /ₒ t
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r : R<VAR>s t : ↥S<GOAL>↑s -ₒ t + (r -ₒ s) = r -ₒ t
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s t : ↥S<GOAL>(r₁ * ↑s /ₒ t) • (r₂ /ₒ s) = r₁ • r₂ /ₒ t
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>r₁ : R<VAR>r₂ : X<VAR>s t : ↥S<GOAL>r₁ + ↑s -ₒ t +ᵥ (r₂ -ₒ s) = r₁ +ᵥ r₂ -ₒ t
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r₁ r₂ : R<VAR>s t : ↥S<GOAL>r₁ + ↑s -ₒ t + (r₂ -ₒ s) = r₁ + r₂ -ₒ t
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r₁ r₂ : R<VAR>s t : ↥S<GOAL>r₁ * ↑s /ₒ t * (r₂ /ₒ s) = r₁ * r₂ /ₒ t
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>MulAction R X<VAR>p : R<VAR>r : X<VAR>s : ↥S<GOAL>(p /ₒ s) • (r /ₒ 1) = p • r /ₒ s
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>X : Type u_2<VAR>AddAction R X<VAR>p : R<VAR>r : X<VAR>s : ↥S<GOAL>p -ₒ s +ᵥ (r -ₒ 0) = p +ᵥ r -ₒ s
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>p r : R<VAR>s : ↥S<GOAL>p -ₒ s + (r -ₒ 0) = p + r -ₒ s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>p r : R<VAR>s : ↥S<GOAL>p /ₒ s * (r /ₒ 1) = p * r /ₒ s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r : R<GOAL>OreLocalization.numeratorHom r = r /ₒ 1
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r : R<GOAL>AddOreLocalization.numeratorHom r = r -ₒ 0
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>s : ↥S<GOAL>IsUnit (OreLocalization.numeratorHom ↑s)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>s : ↥S<GOAL>IsAddUnit (AddOreLocalization.numeratorHom ↑s)
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>T : Type u_2<VAR>AddMonoid T<VAR>f : R →+ T<VAR>fS : ↥S →+ AddUnits T<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<VAR>s : ↥S<GOAL>(AddOreLocalization.universalAddHom f fS hf) (r -ₒ s) = ↑(-fS s) + f r
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>T : Type u_2<VAR>Monoid T<VAR>f : R →* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<VAR>s : ↥S<GOAL>(OreLocalization.universalMulHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>T : Type u_2<VAR>AddMonoid T<VAR>f : R →+ T<VAR>fS : ↥S →+ AddUnits T<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<GOAL>(AddOreLocalization.universalAddHom f fS hf) (AddOreLocalization.numeratorHom r) = f r
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>T : Type u_2<VAR>Monoid T<VAR>f : R →* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<GOAL>(OreLocalization.universalMulHom f fS hf) (OreLocalization.numeratorHom r) = f r
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>T : Type u_2<VAR>Monoid T<VAR>f : R →* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>φ : OreLocalization S R →* T<VAR>huniv : ∀ (r : R), φ (OreLocalization.numeratorHom r) = f r<GOAL>φ = OreLocalization.universalMulHom f fS hf
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>T : Type u_2<VAR>AddMonoid T<VAR>f : R →+ T<VAR>fS : ↥S →+ AddUnits T<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>φ : AddOreLocalization S R →+ T<VAR>huniv : ∀ (r : R), φ (AddOreLocalization.numeratorHom r) = f r<GOAL>φ = AddOreLocalization.universalAddHom f fS hf
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>AddOreLocalization.AddOreSet S<VAR>AddAction M X<VAR>VAdd R X<VAR>VAdd R M<VAR>VAddAssocClass R M M<VAR>VAddAssocClass R M X<VAR>r : R<VAR>x : X<VAR>s : ↥S<GOAL>r +ᵥ (x -ₒ s) = AddOreLocalization.oreMin (r +ᵥ 0) s +ᵥ x -ₒ AddOreLocalization.oreSubtra (r +ᵥ 0) s
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>Monoid M<VAR>S : Submonoid M<VAR>OreLocalization.OreSet S<VAR>MulAction M X<VAR>SMul R X<VAR>SMul R M<VAR>IsScalarTower R M M<VAR>IsScalarTower R M X<VAR>r : R<VAR>x : X<VAR>s : ↥S<GOAL>r • (x /ₒ s) = OreLocalization.oreNum (r • 1) s • x /ₒ OreLocalization.oreDenom (r • 1) s
<VAR>M : Type u_3<VAR>X : Type u_4<VAR>Monoid M<VAR>S : Submonoid M<VAR>OreLocalization.OreSet S<VAR>MulAction M X<VAR>r : M<VAR>x : OreLocalization S X<GOAL>(r /ₒ 1) • x = r • x
<VAR>M : Type u_3<VAR>X : Type u_4<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>AddOreLocalization.AddOreSet S<VAR>AddAction M X<VAR>r : M<VAR>x : AddOreLocalization S X<GOAL>r -ₒ 0 +ᵥ x = r +ᵥ x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>Monoid M<VAR>S : Submonoid M<VAR>OreLocalization.OreSet S<VAR>MulAction M X<VAR>SMul R X<VAR>SMul R M<VAR>IsScalarTower R M M<VAR>IsScalarTower R M X<VAR>r : R<VAR>x : OreLocalization S X<GOAL>(r • 1) • x = r • x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>AddOreLocalization.AddOreSet S<VAR>AddAction M X<VAR>VAdd R X<VAR>VAdd R M<VAR>VAddAssocClass R M M<VAR>VAddAssocClass R M X<VAR>r : R<VAR>x : AddOreLocalization S X<GOAL>r +ᵥ 0 +ᵥ x = r +ᵥ x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>Monoid M<VAR>S : Submonoid M<VAR>OreLocalization.OreSet S<VAR>MulAction M X<VAR>SMul R X<VAR>SMul R M<VAR>IsScalarTower R M M<VAR>IsScalarTower R M X<VAR>r : R<VAR>x : OreLocalization S X<GOAL>(r • 1 /ₒ 1) • x = r • x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>AddOreLocalization.AddOreSet S<VAR>AddAction M X<VAR>VAdd R X<VAR>VAdd R M<VAR>VAddAssocClass R M M<VAR>VAddAssocClass R M X<VAR>r : R<VAR>x : AddOreLocalization S X<GOAL>r +ᵥ 0 -ₒ 0 +ᵥ x = r +ᵥ x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>Monoid M<VAR>S : Submonoid M<VAR>OreLocalization.OreSet S<VAR>MulAction M X<VAR>SMul R X<VAR>SMul R M<VAR>IsScalarTower R M M<VAR>IsScalarTower R M X<VAR>r : R<VAR>x : X<GOAL>r • (x /ₒ 1) = r • x /ₒ 1
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>X : Type u_4<VAR>AddMonoid M<VAR>S : AddSubmonoid M<VAR>AddOreLocalization.AddOreSet S<VAR>AddAction M X<VAR>VAdd R X<VAR>VAdd R M<VAR>VAddAssocClass R M M<VAR>VAddAssocClass R M X<VAR>r : R<VAR>x : X<GOAL>r +ᵥ (x -ₒ 0) = r +ᵥ x -ₒ 0