Documentation

Mathlib.RingTheory.OreLocalization.Basic

Localization over left Ore sets. #

This file defines the localization of a monoid over a left Ore set and proves its universal mapping property.

Notations #

Introduces the notation R[S⁻¹] for the Ore localization of a monoid R at a right Ore subset S. Also defines a new heterogeneous division notation r /ₒ s for a numerator r : R and a denominator s : S.

References #

Tags #

localization, Ore, non-commutative

The setoid on R × S used for the Ore localization.

Equations
Instances For
    theorem AddOreLocalization.oreEqv.proof_1 {R : Type u_1} [AddMonoid R] (S : AddSubmonoid R) [AddOreLocalization.AddOreSet S] (X : Type u_2) [AddAction R X] :
    Equivalence fun (rs rs' : X × S) => ∃ (u : S) (v : R), u +ᵥ rs'.1 = v +ᵥ rs.1 u + rs'.2 = v + rs.2
    def OreLocalization.oreEqv {R : Type u_1} [Monoid R] (S : Submonoid R) [OreLocalization.OreSet S] (X : Type u_2) [MulAction R X] :
    Setoid (X × S)

    The setoid on R × S used for the Ore localization.

    Equations
    Instances For
      def AddOreLocalization {R : Type u_1} [AddMonoid R] (S : AddSubmonoid R) [AddOreLocalization.AddOreSet S] (X : Type u_2) [AddAction R X] :
      Type (max u_1 u_2)

      The Ore localization of an additive monoid and a submonoid fulfilling the Ore condition.

      Equations
      Instances For
        def OreLocalization {R : Type u_1} [Monoid R] (S : Submonoid R) [OreLocalization.OreSet S] (X : Type u_2) [MulAction R X] :
        Type (max u_1 u_2)

        The Ore localization of a monoid and a submonoid fulfilling the Ore condition.

        Equations
        Instances For

          The Ore localization of a monoid and a submonoid fulfilling the Ore condition.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def AddOreLocalization.oreSub {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r : X) (s : S) :

            The subtraction in the Ore localization, as a difference of an element of X and S.

            Equations
            Instances For
              def OreLocalization.oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (r : X) (s : S) :

              The division in the Ore localization X[S⁻¹], as a fraction of an element of X and S.

              Equations
              Instances For

                The division in the Ore localization X[S⁻¹], as a fraction of an element of X and S.

                Equations
                Instances For

                  The subtraction in the Ore localization, as a difference of an element of X and S.

                  Equations
                  Instances For
                    theorem AddOreLocalization.ind {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {β : AddOreLocalization S XProp} (c : ∀ (r : X) (s : S), β (r -ₒ s)) (q : AddOreLocalization S X) :
                    β q
                    theorem OreLocalization.ind {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {β : OreLocalization S XProp} (c : ∀ (r : X) (s : S), β (r /ₒ s)) (q : OreLocalization S X) :
                    β q
                    theorem AddOreLocalization.oreSub_eq_iff {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ : X} {r₂ : X} {s₁ : S} {s₂ : S} :
                    r₁ -ₒ s₁ = r₂ -ₒ s₂ ∃ (u : S) (v : R), u +ᵥ r₂ = v +ᵥ r₁ u + s₂ = v + s₁
                    theorem OreLocalization.oreDiv_eq_iff {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {r₁ : X} {r₂ : X} {s₁ : S} {s₂ : S} :
                    r₁ /ₒ s₁ = r₂ /ₒ s₂ ∃ (u : S) (v : R), u r₂ = v r₁ u * s₂ = v * s₁
                    theorem AddOreLocalization.expand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r : X) (s : S) (t : R) (hst : t + s S) :
                    r -ₒ s = t +ᵥ r -ₒ t + s, hst

                    A difference r -ₒ s is equal to its expansion by an arbitrary translation t if t + s ∈ S.

                    theorem OreLocalization.expand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (r : X) (s : S) (t : R) (hst : t * s S) :
                    r /ₒ s = t r /ₒ t * s, hst

                    A fraction r /ₒ s is equal to its expansion by an arbitrary factor t if t * s ∈ S.

                    theorem AddOreLocalization.expand' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r : X) (s : S) (s' : S) :
                    r -ₒ s = s' +ᵥ r -ₒ (s' + s)

                    A difference is equal to its expansion by a summand from S.

                    theorem OreLocalization.expand' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (r : X) (s : S) (s' : S) :
                    r /ₒ s = s' r /ₒ (s' * s)

                    A fraction is equal to its expansion by a factor from S.

                    theorem AddOreLocalization.eq_of_num_factor_eq {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r : R} {r' : R} {r₁ : R} {r₂ : R} {s : S} {t : S} (h : t + r = t + r') :
                    r₁ + r + r₂ -ₒ s = r₁ + r' + r₂ -ₒ s

                    Differences whose minuends differ by a common summand can be proven equal if those summands expand to equal elements of R.

                    theorem OreLocalization.eq_of_num_factor_eq {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {r' : R} {r₁ : R} {r₂ : R} {s : S} {t : S} (h : t * r = t * r') :
                    r₁ * r * r₂ /ₒ s = r₁ * r' * r₂ /ₒ s

                    Fractions which differ by a factor of the numerator can be proven equal if those factors expand to equal elements of R.

                    abbrev AddOreLocalization.liftExpand.match_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) (motive : (r₁, s₁) (r₂, s₂)Prop) :
                    ∀ (x : (r₁, s₁) (r₂, s₂)), (∀ (u : S) (v : R) (hr₂ : u +ᵥ (r₂, s₂).1 = v +ᵥ (r₁, s₁).1) (hs₂ : u + (r₂, s₂).2 = v + (r₁, s₁).2), motive )motive x
                    Equations
                    • =
                    Instances For
                      abbrev AddOreLocalization.liftExpand.match_3 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_1} [AddAction R X] :
                      ∀ (x : X × S) (motive : (x_1 : X × S) → x_1 xProp) (x_1 : X × S) (x_2 : x_1 x), (∀ (r₁ : X) (s₁ : S) (x : (r₁, s₁) x), motive (r₁, s₁) x)motive x_1 x_2
                      Equations
                      • =
                      Instances For
                        theorem AddOreLocalization.liftExpand.proof_1 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_1} [AddAction R X] {C : Sort u_3} (P : XSC) (hP : ∀ (r : X) (t : R) (s : S) (ht : t + s S), P r s = P (t +ᵥ r) t + s, ht) :
                        ∀ (x x_1 : X × S), x x_1(fun (p : X × S) => P p.1 p.2) x = (fun (p : X × S) => P p.1 p.2) x_1
                        abbrev AddOreLocalization.liftExpand.match_2 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_1} [AddAction R X] (r₁ : X) (s₁ : S) (motive : (x : X × S) → (r₁, s₁) xProp) :
                        ∀ (x : X × S) (x_1 : (r₁, s₁) x), (∀ (r₂ : X) (s₂ : S) (x : (r₁, s₁) (r₂, s₂)), motive (r₂, s₂) x)motive x x_1
                        Equations
                        • =
                        Instances For
                          def AddOreLocalization.liftExpand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} (P : XSC) (hP : ∀ (r : X) (t : R) (s : S) (ht : t + s S), P r s = P (t +ᵥ r) t + s, ht) :

                          A function or predicate over X and S can be lifted to the localizaton if it is invariant under expansion on the left.

                          Equations
                          Instances For
                            def OreLocalization.liftExpand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} (P : XSC) (hP : ∀ (r : X) (t : R) (s : S) (ht : t * s S), P r s = P (t r) t * s, ht) :
                            OreLocalization S XC

                            A function or predicate over X and S can be lifted to X[S⁻¹] if it is invariant under expansion on the left.

                            Equations
                            Instances For
                              @[simp]
                              theorem AddOreLocalization.liftExpand_of {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} {P : XSC} {hP : ∀ (r : X) (t : R) (s : S) (ht : t + s S), P r s = P (t +ᵥ r) t + s, ht} (r : X) (s : S) :
                              @[simp]
                              theorem OreLocalization.liftExpand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} {P : XSC} {hP : ∀ (r : X) (t : R) (s : S) (ht : t * s S), P r s = P (t r) t * s, ht} (r : X) (s : S) :
                              theorem AddOreLocalization.lift₂Expand.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} {X : Type u_3} [AddAction R X] {C : Sort u_2} (P : XSXSC) (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₂) (r₁ : X) (s₁ : S) (r₂ : X) (t₂ : R) (s₂ : S) (ht₂ : t₂ + s₂ S) :
                              P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ +ᵥ r₂) t₂ + s₂, ht₂
                              def AddOreLocalization.lift₂Expand {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} (P : XSXSC) (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₂) :

                              A version of liftExpand used to simultaneously lift functions with two arguments

                              Equations
                              Instances For
                                theorem AddOreLocalization.lift₂Expand.proof_2 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {C : Sort u_3} (P : XSXSC) (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₂) (r₁ : X) (t₁ : R) (s₁ : S) (ht₁ : t₁ + s₁ S) :
                                (fun (r₁ : X) (s₁ : S) => AddOreLocalization.liftExpand (P r₁ s₁) ) r₁ s₁ = (fun (r₁ : X) (s₁ : S) => AddOreLocalization.liftExpand (P r₁ s₁) ) (t₁ +ᵥ r₁) t₁ + s₁, ht₁
                                def OreLocalization.lift₂Expand {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} (P : XSXSC) (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₂) :

                                A version of liftExpand used to simultaneously lift functions with two arguments in X[S⁻¹].

                                Equations
                                Instances For
                                  @[simp]
                                  theorem AddOreLocalization.lift₂Expand_of {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_3} [AddAction R X] {C : Sort u_2} {P : XSXSC} {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₂} (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) :
                                  AddOreLocalization.lift₂Expand P hP (r₁ -ₒ s₁) (r₂ -ₒ s₂) = P r₁ s₁ r₂ s₂
                                  @[simp]
                                  theorem OreLocalization.lift₂Expand_of {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_3} [MulAction R X] {C : Sort u_2} {P : XSXSC} {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₂} (r₁ : X) (s₁ : S) (r₂ : X) (s₂ : S) :
                                  OreLocalization.lift₂Expand P hP (r₁ /ₒ s₁) (r₂ /ₒ s₂) = P r₁ s₁ r₂ s₂
                                  theorem AddOreLocalization.vadd.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : R) (s : S) (hs : r₂ + s S) :
                                  OreLocalization.vadd'' r₁ s = OreLocalization.vadd'' (r₂ +ᵥ r₁) r₂ + s, hs
                                  @[irreducible]

                                  the vector addition on the Ore localization of additive monoids.

                                  Equations
                                  Instances For
                                    @[irreducible]

                                    The scalar multiplication on the Ore localization of monoids.

                                    Equations
                                    Instances For
                                      Equations
                                      • AddOreLocalization.instVAdd = { vadd := AddOreLocalization.vadd }
                                      Equations
                                      • OreLocalization.instSMul = { smul := OreLocalization.smul }
                                      Equations
                                      • AddOreLocalization.instAdd = { add := AddOreLocalization.vadd }
                                      Equations
                                      • OreLocalization.instMul = { mul := OreLocalization.smul }
                                      theorem AddOreLocalization.oreSub_vadd_oreSub {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ : R} {r₂ : X} {s₁ : S} {s₂ : S} :
                                      r₁ -ₒ s₁ +ᵥ (r₂ -ₒ s₂) = AddOreLocalization.oreMin r₁ s₂ +ᵥ r₂ -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
                                      theorem OreLocalization.oreDiv_smul_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {r₁ : R} {r₂ : X} {s₁ : S} {s₂ : S} :
                                      (r₁ /ₒ s₁) (r₂ /ₒ s₂) = OreLocalization.oreNum r₁ s₂ r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)
                                      theorem AddOreLocalization.oreSub_add_oreSub {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r₁ : R} {r₂ : R} {s₁ : S} {s₂ : S} :
                                      r₁ -ₒ s₁ + (r₂ -ₒ s₂) = AddOreLocalization.oreMin r₁ s₂ + r₂ -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
                                      theorem OreLocalization.oreDiv_mul_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s₁ : S} {s₂ : S} :
                                      r₁ /ₒ s₁ * (r₂ /ₒ s₂) = OreLocalization.oreNum r₁ s₂ * r₂ /ₒ (OreLocalization.oreDenom r₁ s₂ * s₁)
                                      theorem AddOreLocalization.oreSub_vadd_char {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : X) (s₁ : S) (s₂ : S) (r' : R) (s' : S) (huv : s' + r₁ = r' + s₂) :
                                      r₁ -ₒ s₁ +ᵥ (r₂ -ₒ s₂) = r' +ᵥ r₂ -ₒ (s' + s₁)

                                      A characterization lemma for the vector addition on the Ore localization, allowing for a choice of Ore minuend and Ore subtrahend.

                                      theorem OreLocalization.oreDiv_smul_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (r₁ : R) (r₂ : X) (s₁ : S) (s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
                                      (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' r₂ /ₒ (s' * s₁)

                                      A characterization lemma for the scalar multiplication on the Ore localization, allowing for a choice of Ore numerator and Ore denominator.

                                      theorem AddOreLocalization.oreSub_add_char {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s₁ : S) (s₂ : S) (r' : R) (s' : S) (huv : s' + r₁ = r' + s₂) :
                                      r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r' + r₂ -ₒ (s' + s₁)

                                      A characterization lemma for the addition on the Ore localization, allowing for a choice of Ore minuend and Ore subtrahend.

                                      theorem OreLocalization.oreDiv_mul_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r₁ : R) (r₂ : R) (s₁ : S) (s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
                                      r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

                                      A characterization lemma for the multiplication on the Ore localization, allowing for a choice of Ore numerator and Ore denominator.

                                      def AddOreLocalization.oreSubVAddChar' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : X) (s₁ : S) (s₂ : S) :
                                      (r' : R) ×' (s' : S) ×' s' + r₁ = r' + s₂ r₁ -ₒ s₁ +ᵥ (r₂ -ₒ s₂) = r' +ᵥ r₂ -ₒ (s' + s₁)

                                      Another characterization lemma for the vector addition on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.

                                      Equations
                                      Instances For
                                        theorem AddOreLocalization.oreSubVAddChar'.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] (r₁ : R) (r₂ : X) (s₁ : S) (s₂ : S) :
                                        (AddOreLocalization.oreSubtra r₁ s₂) + r₁ = AddOreLocalization.oreMin r₁ s₂ + s₂ r₁ -ₒ s₁ +ᵥ (r₂ -ₒ s₂) = AddOreLocalization.oreMin r₁ s₂ +ᵥ r₂ -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
                                        def OreLocalization.oreDivSMulChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (r₁ : R) (r₂ : X) (s₁ : S) (s₂ : S) :
                                        (r' : R) ×' (s' : S) ×' s' * r₁ = r' * s₂ (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r' r₂ /ₒ (s' * s₁)

                                        Another characterization lemma for the scalar multiplication on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.

                                        Equations
                                        Instances For
                                          theorem AddOreLocalization.oreSubAddChar'.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s₁ : S) (s₂ : S) :
                                          (AddOreLocalization.oreSubtra r₁ s₂) + r₁ = AddOreLocalization.oreMin r₁ s₂ + s₂ r₁ -ₒ s₁ + (r₂ -ₒ s₂) = AddOreLocalization.oreMin r₁ s₂ + r₂ -ₒ (AddOreLocalization.oreSubtra r₁ s₂ + s₁)
                                          def AddOreLocalization.oreSubAddChar' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (r₁ : R) (r₂ : R) (s₁ : S) (s₂ : S) :
                                          (r' : R) ×' (s' : S) ×' s' + r₁ = r' + s₂ r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r' + r₂ -ₒ (s' + s₁)

                                          Another characterization lemma for the addition on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.

                                          Equations
                                          Instances For
                                            def OreLocalization.oreDivMulChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (r₁ : R) (r₂ : R) (s₁ : S) (s₂ : S) :
                                            (r' : R) ×' (s' : S) ×' s' * r₁ = r' * s₂ r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r' * r₂ /ₒ (s' * s₁)

                                            Another characterization lemma for the multiplication on the Ore localizaion delivering Ore witnesses and conditions bundled in a sigma type.

                                            Equations
                                            Instances For
                                              @[irreducible]

                                              0 in the additive localization, defined as 0 -ₒ 0.

                                              Equations
                                              • AddOreLocalization.zero = 0 -ₒ 0
                                              Instances For
                                                @[irreducible]

                                                1 in the localization, defined as 1 /ₒ 1.

                                                Equations
                                                • OreLocalization.one = 1 /ₒ 1
                                                Instances For
                                                  Equations
                                                  • AddOreLocalization.instZero = { zero := AddOreLocalization.zero }
                                                  Equations
                                                  • OreLocalization.instOne = { one := OreLocalization.one }
                                                  Equations
                                                  • AddOreLocalization.instInhabited = { default := 0 }
                                                  Equations
                                                  • OreLocalization.instInhabited = { default := 1 }
                                                  @[simp]
                                                  theorem AddOreLocalization.sub_eq_zero' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r : R} (hr : r S) :
                                                  r -ₒ r, hr = 0
                                                  @[simp]
                                                  theorem OreLocalization.div_eq_one' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} (hr : r S) :
                                                  r /ₒ r, hr = 1
                                                  @[simp]
                                                  theorem AddOreLocalization.sub_eq_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {s : S} :
                                                  s -ₒ s = 0
                                                  @[simp]
                                                  theorem OreLocalization.div_eq_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {s : S} :
                                                  s /ₒ s = 1
                                                  theorem OreLocalization.one_smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (x : OreLocalization S X) :
                                                  1 x = x
                                                  theorem OreLocalization.one_mul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization S R) :
                                                  1 * x = x
                                                  theorem OreLocalization.mul_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization S R) :
                                                  x * 1 = x
                                                  theorem OreLocalization.mul_smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] (x : OreLocalization S R) (y : OreLocalization S R) (z : OreLocalization S X) :
                                                  (x * y) z = x y z
                                                  theorem OreLocalization.mul_assoc {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (x : OreLocalization S R) (y : OreLocalization S R) (z : OreLocalization S R) :
                                                  x * y * z = x * (y * z)
                                                  @[irreducible]

                                                  nsmul of AddOreLocalization

                                                  Equations
                                                  • AddOreLocalization.nsmul = nsmulRec
                                                  Instances For
                                                    @[irreducible]

                                                    npow of OreLocalization

                                                    Equations
                                                    • OreLocalization.npow = npowRec
                                                    Instances For
                                                      Equations
                                                      • AddOreLocalization.instAddMonoid = AddMonoid.mk AddOreLocalization.nsmul
                                                      Equations
                                                      • OreLocalization.instMonoid = Monoid.mk OreLocalization.npow
                                                      Equations
                                                      • AddOreLocalization.instAddActionOreLocalization = AddAction.mk
                                                      Equations
                                                      • OreLocalization.instMulActionOreLocalization = MulAction.mk
                                                      theorem AddOreLocalization.add_neg {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (s : S) (s' : S) :
                                                      s -ₒ s' + (s' -ₒ s) = 0
                                                      theorem OreLocalization.mul_inv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (s : S) (s' : S) :
                                                      s /ₒ s' * (s' /ₒ s) = 1
                                                      @[simp]
                                                      theorem AddOreLocalization.zero_sub_vadd {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r : X} {s : S} {t : S} :
                                                      0 -ₒ t +ᵥ (r -ₒ s) = r -ₒ (s + t)
                                                      @[simp]
                                                      theorem OreLocalization.one_div_smul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {r : X} {s : S} {t : S} :
                                                      (1 /ₒ t) (r /ₒ s) = r /ₒ (s * t)
                                                      @[simp]
                                                      theorem AddOreLocalization.zero_sub_add {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r : R} {s : S} {t : S} :
                                                      0 -ₒ t + (r -ₒ s) = r -ₒ (s + t)
                                                      @[simp]
                                                      theorem OreLocalization.one_div_mul {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {s : S} {t : S} :
                                                      1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)
                                                      @[simp]
                                                      theorem AddOreLocalization.vadd_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r : X} {s : S} {t : S} :
                                                      s -ₒ t +ᵥ (r -ₒ s) = r -ₒ t
                                                      @[simp]
                                                      theorem OreLocalization.smul_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {r : X} {s : S} {t : S} :
                                                      (s /ₒ t) (r /ₒ s) = r /ₒ t
                                                      @[simp]
                                                      theorem AddOreLocalization.add_cancel {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r : R} {s : S} {t : S} :
                                                      s -ₒ t + (r -ₒ s) = r -ₒ t
                                                      @[simp]
                                                      theorem OreLocalization.mul_cancel {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} {s : S} {t : S} :
                                                      s /ₒ t * (r /ₒ s) = r /ₒ t
                                                      @[simp]
                                                      theorem AddOreLocalization.vadd_cancel' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {r₁ : R} {r₂ : X} {s : S} {t : S} :
                                                      r₁ + s -ₒ t +ᵥ (r₂ -ₒ s) = r₁ +ᵥ r₂ -ₒ t
                                                      @[simp]
                                                      theorem OreLocalization.smul_cancel' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {r₁ : R} {r₂ : X} {s : S} {t : S} :
                                                      (r₁ * s /ₒ t) (r₂ /ₒ s) = r₁ r₂ /ₒ t
                                                      @[simp]
                                                      theorem AddOreLocalization.add_cancel' {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r₁ : R} {r₂ : R} {s : S} {t : S} :
                                                      r₁ + s -ₒ t + (r₂ -ₒ s) = r₁ + r₂ -ₒ t
                                                      @[simp]
                                                      theorem OreLocalization.mul_cancel' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s : S} {t : S} :
                                                      r₁ * s /ₒ t * (r₂ /ₒ s) = r₁ * r₂ /ₒ t
                                                      @[simp]
                                                      theorem AddOreLocalization.vadd_sub_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {X : Type u_2} [AddAction R X] {p : R} {r : X} {s : S} :
                                                      p -ₒ s +ᵥ (r -ₒ 0) = p +ᵥ r -ₒ s
                                                      @[simp]
                                                      theorem OreLocalization.smul_div_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [MulAction R X] {p : R} {r : X} {s : S} :
                                                      (p /ₒ s) (r /ₒ 1) = p r /ₒ s
                                                      @[simp]
                                                      theorem AddOreLocalization.add_sub_zero {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {p : R} {r : R} {s : S} :
                                                      p -ₒ s + (r -ₒ 0) = p + r -ₒ s
                                                      @[simp]
                                                      theorem OreLocalization.mul_div_one {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {p : R} {r : R} {s : S} :
                                                      p /ₒ s * (r /ₒ 1) = p * r /ₒ s

                                                      The difference s -ₒ 0 as a an additive unit.

                                                      Equations
                                                      Instances For

                                                        The fraction s /ₒ 1 as a unit in R[S⁻¹], where s : S.

                                                        Equations
                                                        Instances For
                                                          theorem AddOreLocalization.numeratorHom.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] :
                                                          (fun (r : R) => r -ₒ 0) 0 = (fun (r : R) => r -ₒ 0) 0

                                                          The additive homomorphism from R to AddOreLocalization R S, mapping r : R to the difference r -ₒ 0.

                                                          Equations
                                                          • AddOreLocalization.numeratorHom = { toFun := fun (r : R) => r -ₒ 0, map_zero' := , map_add' := }
                                                          Instances For
                                                            theorem AddOreLocalization.numeratorHom.proof_2 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] :
                                                            ∀ (x x_1 : R), x + x_1 -ₒ 0 = x -ₒ 0 + (x_1 -ₒ 0)

                                                            The multiplicative homomorphism from R to R[S⁻¹], mapping r : R to the fraction r /ₒ 1.

                                                            Equations
                                                            • OreLocalization.numeratorHom = { toFun := fun (r : R) => r /ₒ 1, map_one' := , map_mul' := }
                                                            Instances For
                                                              theorem AddOreLocalization.numeratorHom_apply {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r : R} :
                                                              AddOreLocalization.numeratorHom r = r -ₒ 0
                                                              theorem OreLocalization.numeratorHom_apply {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r : R} :
                                                              OreLocalization.numeratorHom r = r /ₒ 1
                                                              theorem AddOreLocalization.numerator_isAddUnit {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] (s : S) :
                                                              IsAddUnit (AddOreLocalization.numeratorHom s)
                                                              theorem OreLocalization.numerator_isUnit {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] (s : S) :
                                                              IsUnit (OreLocalization.numeratorHom s)
                                                              def AddOreLocalization.universalAddHom {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : S →+ AddUnits T) (hf : ∀ (s : S), f s = (fS s)) :

                                                              The universal lift from a morphism R →+ T, which maps elements of S to additive-units of T, to a morphism AddOreLocalization R S →+ T.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                theorem AddOreLocalization.universalAddHom.proof_3 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : S →+ AddUnits T) (hf : ∀ (s : S), f s = (fS s)) (x : AddOreLocalization S R) (y : AddOreLocalization S R) :
                                                                { toFun := fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : S) => (-fS s) + f r) x, map_zero' := }.toFun (x + y) = { toFun := fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : S) => (-fS s) + f r) x, map_zero' := }.toFun x + { toFun := fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : S) => (-fS s) + f r) x, map_zero' := }.toFun y
                                                                theorem AddOreLocalization.universalAddHom.proof_2 {R : Type u_2} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_1} [AddMonoid T] (f : R →+ T) (fS : S →+ AddUnits T) (hf : ∀ (s : S), f s = (fS s)) :
                                                                (fun (x : AddOreLocalization S R) => AddOreLocalization.liftExpand (fun (r : R) (s : S) => (-fS s) + f r) x) 0 = 0
                                                                theorem AddOreLocalization.universalAddHom.proof_1 {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : S →+ AddUnits T) (hf : ∀ (s : S), f s = (fS s)) (r : R) (t : R) (s : S) (ht : t + s S) :
                                                                (fun (r : R) (s : S) => (-fS s) + f r) r s = (fun (r : R) (s : S) => (-fS s) + f r) (t +ᵥ r) t + s, ht
                                                                def OreLocalization.universalMulHom {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) :

                                                                The universal lift from a morphism R →* T, which maps elements of S to units of T, to a morphism R[S⁻¹] →* T.

                                                                Equations
                                                                Instances For
                                                                  theorem AddOreLocalization.universalAddHom_apply {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : S →+ AddUnits T) (hf : ∀ (s : S), f s = (fS s)) {r : R} {s : S} :
                                                                  (AddOreLocalization.universalAddHom f fS hf) (r -ₒ s) = (-fS s) + f r
                                                                  theorem OreLocalization.universalMulHom_apply {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) {r : R} {s : S} :
                                                                  (OreLocalization.universalMulHom f fS hf) (r /ₒ s) = (fS s)⁻¹ * f r
                                                                  theorem AddOreLocalization.universalAddHom_commutes {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : S →+ AddUnits T) (hf : ∀ (s : S), f s = (fS s)) {r : R} :
                                                                  (AddOreLocalization.universalAddHom f fS hf) (AddOreLocalization.numeratorHom r) = f r
                                                                  theorem OreLocalization.universalMulHom_commutes {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) {r : R} :
                                                                  (OreLocalization.universalMulHom f fS hf) (OreLocalization.numeratorHom r) = f r
                                                                  theorem AddOreLocalization.universalAddHom_unique {R : Type u_1} [AddMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {T : Type u_2} [AddMonoid T] (f : R →+ T) (fS : S →+ AddUnits T) (hf : ∀ (s : S), f s = (fS s)) (φ : AddOreLocalization S R →+ T) (huniv : ∀ (r : R), φ (AddOreLocalization.numeratorHom r) = f r) :

                                                                  The universal morphism universalAddHom is unique.

                                                                  theorem OreLocalization.universalMulHom_unique {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {T : Type u_2} [Monoid T] (f : R →* T) (fS : S →* Tˣ) (hf : ∀ (s : S), f s = (fS s)) (φ : OreLocalization S R →* T) (huniv : ∀ (r : R), φ (OreLocalization.numeratorHom r) = f r) :

                                                                  The universal morphism universalMulHom is unique.

                                                                  theorem AddOreLocalization.hvadd.proof_1 {R : Type u_3} {M : Type u_1} {X : Type u_2} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R M] (c : R) (r : X) (t : M) (s : S) (ht : t + s S) :
                                                                  (fun (m : X) (s : S) => AddOreLocalization.oreMin (c +ᵥ 0) s +ᵥ m -ₒ AddOreLocalization.oreSubtra (c +ᵥ 0) s) r s = (fun (m : X) (s : S) => AddOreLocalization.oreMin (c +ᵥ 0) s +ᵥ m -ₒ AddOreLocalization.oreSubtra (c +ᵥ 0) s) (t +ᵥ r) t + s, ht
                                                                  @[irreducible]
                                                                  def AddOreLocalization.hvadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R M] (c : R) :

                                                                  Vector addition in an additive monoid localization.

                                                                  Equations
                                                                  Instances For
                                                                    @[irreducible]
                                                                    def OreLocalization.hsmul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R M] (c : R) :

                                                                    Scalar multiplication in a monoid localization.

                                                                    Equations
                                                                    Instances For
                                                                      Equations
                                                                      • AddOreLocalization.instVAddOfIsScalarTower = { vadd := AddOreLocalization.hvadd }
                                                                      instance OreLocalization.instSMulOfIsScalarTower {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M X] [IsScalarTower R M M] :
                                                                      Equations
                                                                      • OreLocalization.instSMulOfIsScalarTower = { smul := OreLocalization.hsmul }
                                                                      theorem AddOreLocalization.vadd_oreSub {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : X) (s : S) :
                                                                      theorem OreLocalization.smul_oreDiv {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : X) (s : S) :
                                                                      @[simp]
                                                                      theorem AddOreLocalization.oreSub_zero_vadd {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] (r : M) (x : AddOreLocalization S X) :
                                                                      r -ₒ 0 +ᵥ x = r +ᵥ x
                                                                      @[simp]
                                                                      theorem OreLocalization.oreDiv_one_smul {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] (r : M) (x : OreLocalization S X) :
                                                                      (r /ₒ 1) x = r x
                                                                      theorem AddOreLocalization.vadd_zero_vadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : AddOreLocalization S X) :
                                                                      r +ᵥ 0 +ᵥ x = r +ᵥ x
                                                                      theorem OreLocalization.smul_one_smul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : OreLocalization S X) :
                                                                      (r 1) x = r x
                                                                      theorem AddOreLocalization.vadd_zero_oreSub_zero_vadd {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : AddOreLocalization S X) :
                                                                      r +ᵥ 0 -ₒ 0 +ᵥ x = r +ᵥ x
                                                                      theorem OreLocalization.smul_one_oreDiv_one_smul {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : OreLocalization S X) :
                                                                      (r 1 /ₒ 1) x = r x
                                                                      instance AddOreLocalization.instIsScalarTower {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] [VAdd R' X] [VAdd R' M] [VAddAssocClass R' M M] [VAddAssocClass R' M X] [VAdd R R'] [VAddAssocClass R R' M] :
                                                                      Equations
                                                                      • =
                                                                      instance OreLocalization.instIsScalarTower {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul R' X] [SMul R' M] [IsScalarTower R' M M] [IsScalarTower R' M X] [SMul R R'] [IsScalarTower R R' M] :
                                                                      Equations
                                                                      • =
                                                                      instance AddOreLocalization.instVAddCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] [VAdd R' X] [VAdd R' M] [VAddAssocClass R' M M] [VAddAssocClass R' M X] [VAddCommClass R R' M] :
                                                                      Equations
                                                                      • =
                                                                      instance OreLocalization.instSMulCommClass {R : Type u_1} {R' : Type u_2} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMul R' X] [SMul R' M] [IsScalarTower R' M M] [IsScalarTower R' M X] [SMulCommClass R R' M] :
                                                                      Equations
                                                                      • =
                                                                      Equations
                                                                      • =
                                                                      instance OreLocalization.instIsScalarTower_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] :
                                                                      Equations
                                                                      • =
                                                                      Equations
                                                                      • =
                                                                      instance OreLocalization.instSMulCommClass_1 {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] [SMulCommClass R M M] :
                                                                      Equations
                                                                      • =
                                                                      Equations
                                                                      • =
                                                                      theorem AddOreLocalization.instAddActionOfIsScalarTower.proof_2 {M : Type u_1} {X : Type u_2} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] {R : Type u_3} [AddMonoid R] [AddAction R M] [VAddAssocClass R M M] [AddAction R X] [VAddAssocClass R M X] (s₁ : R) (s₂ : R) (x : AddOreLocalization S X) :
                                                                      s₁ + s₂ +ᵥ x = s₁ +ᵥ (s₂ +ᵥ x)
                                                                      Equations
                                                                      • AddOreLocalization.instAddActionOfIsScalarTower = AddAction.mk
                                                                      Equations
                                                                      • OreLocalization.instMulActionOfIsScalarTower = MulAction.mk
                                                                      theorem AddOreLocalization.vadd_oreSub_zero {R : Type u_1} {M : Type u_3} {X : Type u_4} [AddMonoid M] {S : AddSubmonoid M} [AddOreLocalization.AddOreSet S] [AddAction M X] [VAdd R X] [VAdd R M] [VAddAssocClass R M M] [VAddAssocClass R M X] (r : R) (x : X) :
                                                                      r +ᵥ (x -ₒ 0) = r +ᵥ x -ₒ 0
                                                                      theorem OreLocalization.smul_oreDiv_one {R : Type u_1} {M : Type u_3} {X : Type u_4} [Monoid M] {S : Submonoid M} [OreLocalization.OreSet S] [MulAction M X] [SMul R X] [SMul R M] [IsScalarTower R M M] [IsScalarTower R M X] (r : R) (x : X) :
                                                                      r (x /ₒ 1) = r x /ₒ 1
                                                                      theorem AddOreLocalization.oreSub_add_oreSub_comm {R : Type u_1} [AddCommMonoid R] {S : AddSubmonoid R} [AddOreLocalization.AddOreSet S] {r₁ : R} {r₂ : R} {s₁ : S} {s₂ : S} :
                                                                      r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r₁ + r₂ -ₒ (s₁ + s₂)
                                                                      theorem OreLocalization.oreDiv_mul_oreDiv_comm {R : Type u_1} [CommMonoid R] {S : Submonoid R} [OreLocalization.OreSet S] {r₁ : R} {r₂ : R} {s₁ : S} {s₂ : S} :
                                                                      r₁ /ₒ s₁ * (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)
                                                                      Equations
                                                                      Equations
                                                                      @[irreducible]
                                                                      def OreLocalization.zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [Zero X] [MulAction R X] :

                                                                      0 in the localization, defined as 0 /ₒ 1.

                                                                      Equations
                                                                      • OreLocalization.zero = 0 /ₒ 1
                                                                      Instances For
                                                                        instance OreLocalization.instZero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [Zero X] [MulAction R X] :
                                                                        Equations
                                                                        • OreLocalization.instZero = { zero := OreLocalization.zero }
                                                                        theorem OreLocalization.zero_def {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [Zero X] [MulAction R X] :
                                                                        0 = 0 /ₒ 1
                                                                        @[simp]
                                                                        theorem OreLocalization.zero_oreDiv' {R : Type u_1} [MonoidWithZero R] {S : Submonoid R} [OreLocalization.OreSet S] (s : S) :
                                                                        0 /ₒ s = 0
                                                                        Equations
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Equations
                                                                        • OreLocalization.instAdd = { add := OreLocalization.add }
                                                                        theorem OreLocalization.oreDiv_add_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} {s : S} {s' : S} :
                                                                        r /ₒ s + r' /ₒ s' = (OreLocalization.oreDenom (s) s' r + OreLocalization.oreNum (s) s' r') /ₒ (OreLocalization.oreDenom (s) s' * s)
                                                                        theorem OreLocalization.oreDiv_add_char' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} (s : S) (s' : S) (rb : R) (sb : R) (h : sb * s = rb * s') (h' : sb * s S) :
                                                                        r /ₒ s + r' /ₒ s' = (sb r + rb r') /ₒ sb * s, h'
                                                                        theorem OreLocalization.oreDiv_add_char {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} (s : S) (s' : S) (rb : R) (sb : S) (h : sb * s = rb * s') :
                                                                        r /ₒ s + r' /ₒ s' = (sb r + rb r') /ₒ (sb * s)

                                                                        A characterization of the addition on the Ore localizaion, allowing for arbitrary Ore numerator and Ore denominator.

                                                                        def OreLocalization.oreDivAddChar' {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (r : X) (r' : X) (s : S) (s' : S) :
                                                                        (r'' : R) ×' (s'' : S) ×' s'' * s = r'' * s' r /ₒ s + r' /ₒ s' = (s'' r + r'' r') /ₒ (s'' * s)

                                                                        Another characterization of the addition on the Ore localization, bundling up all witnesses and conditions into a sigma type.

                                                                        Equations
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem OreLocalization.add_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {r : X} {r' : X} {s : S} :
                                                                          r /ₒ s + r' /ₒ s = (r + r') /ₒ s
                                                                          theorem OreLocalization.add_assoc {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) (y : OreLocalization S X) (z : OreLocalization S X) :
                                                                          x + y + z = x + (y + z)
                                                                          @[simp]
                                                                          theorem OreLocalization.zero_oreDiv {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (s : S) :
                                                                          0 /ₒ s = 0
                                                                          theorem OreLocalization.zero_add {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) :
                                                                          0 + x = x
                                                                          theorem OreLocalization.add_zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S X) :
                                                                          x + 0 = x
                                                                          Equations
                                                                          • OreLocalization.instAddMonoid = AddMonoid.mk OreLocalization.nsmul
                                                                          theorem OreLocalization.smul_zero {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (x : OreLocalization S R) :
                                                                          x 0 = 0
                                                                          theorem OreLocalization.smul_add {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] (z : OreLocalization S R) (x : OreLocalization S X) (y : OreLocalization S X) :
                                                                          z (x + y) = z x + z y
                                                                          Equations
                                                                          instance OreLocalization.instDistribMulActionOfIsScalarTower {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddMonoid X] [DistribMulAction R X] {R₀ : Type u_3} [Monoid R₀] [MulAction R₀ X] [MulAction R₀ R] [IsScalarTower R₀ R X] [IsScalarTower R₀ R R] :
                                                                          Equations
                                                                          theorem OreLocalization.add_comm {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddCommMonoid X] [DistribMulAction R X] (x : OreLocalization S X) (y : OreLocalization S X) :
                                                                          x + y = y + x
                                                                          Equations
                                                                          @[irreducible]

                                                                          Negation on the Ore localization is defined via negation on the numerator.

                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            • OreLocalization.instNegOreLocalization = { neg := OreLocalization.neg }
                                                                            @[simp]
                                                                            theorem OreLocalization.neg_def {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] (r : X) (s : S) :
                                                                            -(r /ₒ s) = -r /ₒ s
                                                                            theorem OreLocalization.add_left_neg {R : Type u_1} [Monoid R] {S : Submonoid R} [OreLocalization.OreSet S] {X : Type u_2} [AddGroup X] [DistribMulAction R X] (x : OreLocalization S X) :
                                                                            -x + x = 0
                                                                            @[irreducible]

                                                                            zsmul of OreLocalization

                                                                            Equations
                                                                            • OreLocalization.zsmul = zsmulRec
                                                                            Instances For
                                                                              Equations
                                                                              • OreLocalization.instAddGroupOreLocalization = AddGroup.mk
                                                                              Equations