Documentation

Mathlib.Algebra.Group.Commute.Units

Lemmas about commuting pairs of elements involving units. #

theorem AddCommute.addUnits_neg_right {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute a uAddCommute a (-u)
theorem Commute.units_inv_right {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute a uCommute a u⁻¹
@[simp]
theorem AddCommute.addUnits_neg_right_iff {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute a (-u) AddCommute a u
@[simp]
theorem Commute.units_inv_right_iff {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute a u⁻¹ Commute a u
theorem AddCommute.addUnits_neg_left {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute (u) aAddCommute ((-u)) a
theorem Commute.units_inv_left {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute (u) aCommute (u⁻¹) a
@[simp]
theorem AddCommute.addUnits_neg_left_iff {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute ((-u)) a AddCommute (u) a
@[simp]
theorem Commute.units_inv_left_iff {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute (u⁻¹) a Commute (u) a
theorem AddCommute.addUnits_val {M : Type u_1} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :
AddCommute u₁ u₂AddCommute u₁ u₂
theorem Commute.units_val {M : Type u_1} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute u₁ u₂Commute u₁ u₂
theorem AddCommute.addUnits_of_val {M : Type u_1} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :
AddCommute u₁ u₂AddCommute u₁ u₂
theorem Commute.units_of_val {M : Type u_1} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute u₁ u₂Commute u₁ u₂
@[simp]
theorem AddCommute.addUnits_val_iff {M : Type u_1} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :
AddCommute u₁ u₂ AddCommute u₁ u₂
@[simp]
theorem Commute.units_val_iff {M : Type u_1} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute u₁ u₂ Commute u₁ u₂
theorem AddUnits.leftOfAdd.proof_2 {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = u) (hc : AddCommute a b) :
b + (-u) + a = 0
theorem AddUnits.leftOfAdd.proof_1 {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = u) :
a + (b + (-u)) = 0
def AddUnits.leftOfAdd {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = u) (hc : AddCommute a b) :

If the sum of two commuting elements is an additive unit, then the left summand is an additive unit.

Equations
Instances For
    def Units.leftOfMul {M : Type u_1} [Monoid M] (u : Mˣ) (a : M) (b : M) (hu : a * b = u) (hc : Commute a b) :

    If the product of two commuting elements is a unit, then the left multiplier is a unit.

    Equations
    Instances For
      theorem AddUnits.rightOfAdd.proof_1 {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = u) (hc : AddCommute a b) :
      b + a = u
      theorem AddUnits.rightOfAdd.proof_2 {M : Type u_1} [AddMonoid M] (a : M) (b : M) (hc : AddCommute a b) :
      def AddUnits.rightOfAdd {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = u) (hc : AddCommute a b) :

      If the sum of two commuting elements is an additive unit, then the right summand is an additive unit.

      Equations
      Instances For
        def Units.rightOfMul {M : Type u_1} [Monoid M] (u : Mˣ) (a : M) (b : M) (hu : a * b = u) (hc : Commute a b) :

        If the product of two commuting elements is a unit, then the right multiplier is a unit.

        Equations
        Instances For
          abbrev AddCommute.isAddUnit_add_iff.match_1 {M : Type u_1} [AddMonoid M] {a : M} {b : M} (motive : IsAddUnit (a + b)Prop) :
          ∀ (x : IsAddUnit (a + b)), (∀ (u : AddUnits M) (hu : u = a + b), motive (_ : ∃ (u : AddUnits M), u = a + b))motive x
          Equations
          • (_ : motive x) = (_ : motive x)
          Instances For
            theorem AddCommute.isAddUnit_add_iff {M : Type u_1} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) :
            theorem Commute.isUnit_mul_iff {M : Type u_1} [Monoid M] {a : M} {b : M} (h : Commute a b) :
            @[simp]
            theorem isAddUnit_add_self_iff {M : Type u_1} [AddMonoid M] {a : M} :
            @[simp]
            theorem isUnit_mul_self_iff {M : Type u_1} [Monoid M] {a : M} :
            IsUnit (a * a) IsUnit a
            @[simp]
            theorem AddCommute.addUnits_zsmul_right {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} (h : AddCommute a u) (m : ) :
            AddCommute a (m u)
            @[simp]
            theorem Commute.units_zpow_right {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} (h : Commute a u) (m : ) :
            Commute a (u ^ m)
            @[simp]
            theorem AddCommute.addUnits_zsmul_left {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} (h : AddCommute (u) a) (m : ) :
            AddCommute ((m u)) a
            @[simp]
            theorem Commute.units_zpow_left {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} (h : Commute (u) a) (m : ) :
            Commute ((u ^ m)) a
            def AddUnits.ofNSMul {M : Type u_1} [AddMonoid M] (u : AddUnits M) (x : M) {n : } (hn : n 0) (hu : n x = u) :

            If a natural multiple of x is an additive unit, then x is an additive unit.

            Equations
            Instances For
              theorem AddUnits.ofNSMul.proof_1 {M : Type u_1} [AddMonoid M] (u : AddUnits M) (x : M) {n : } (hn : n 0) (hu : n x = u) :
              x + (n - 1) x = u
              theorem AddUnits.ofNSMul.proof_2 {M : Type u_1} [AddMonoid M] (x : M) {n : } :
              AddCommute x ((n - 1) x)
              def Units.ofPow {M : Type u_1} [Monoid M] (u : Mˣ) (x : M) {n : } (hn : n 0) (hu : x ^ n = u) :

              If a natural power of x is a unit, then x is a unit.

              Equations
              Instances For
                abbrev isAddUnit_nsmul_iff.match_1 {M : Type u_1} [AddMonoid M] {n : } {a : M} (motive : IsAddUnit (n a)Prop) :
                ∀ (x : IsAddUnit (n a)), (∀ (u : AddUnits M) (hu : u = n a), motive (_ : ∃ (u : AddUnits M), u = n a))motive x
                Equations
                • (_ : motive x) = (_ : motive x)
                Instances For
                  @[simp]
                  theorem isAddUnit_nsmul_iff {M : Type u_1} [AddMonoid M] {n : } {a : M} (hn : n 0) :
                  @[simp]
                  theorem isUnit_pow_iff {M : Type u_1} [Monoid M] {n : } {a : M} (hn : n 0) :
                  IsUnit (a ^ n) IsUnit a
                  theorem isAddUnit_nsmul_succ_iff {M : Type u_1} [AddMonoid M] {n : } {a : M} :
                  theorem isUnit_pow_succ_iff {M : Type u_1} [Monoid M] {n : } {a : M} :
                  IsUnit (a ^ (n + 1)) IsUnit a
                  def AddUnits.ofNSMulEqZero {M : Type u_1} [AddMonoid M] (a : M) (n : ) (ha : n a = 0) (hn : n 0) :

                  If n • x = 0, n ≠ 0, then x is an additive unit.

                  Equations
                  Instances For
                    @[simp]
                    theorem AddUnits.val_neg_ofNSMulEqZero {M : Type u_1} [AddMonoid M] (a : M) (n : ) (ha : n a = 0) (hn : n 0) :
                    (-AddUnits.ofNSMulEqZero a n ha hn) = (n - 1) a
                    @[simp]
                    theorem AddUnits.val_ofNSMulEqZero {M : Type u_1} [AddMonoid M] (a : M) (n : ) (ha : n a = 0) (hn : n 0) :
                    (AddUnits.ofNSMulEqZero a n ha hn) = a
                    @[simp]
                    theorem Units.val_ofPowEqOne {M : Type u_1} [Monoid M] (a : M) (n : ) (ha : a ^ n = 1) (hn : n 0) :
                    (Units.ofPowEqOne a n ha hn) = a
                    @[simp]
                    theorem Units.val_inv_ofPowEqOne {M : Type u_1} [Monoid M] (a : M) (n : ) (ha : a ^ n = 1) (hn : n 0) :
                    (Units.ofPowEqOne a n ha hn)⁻¹ = a ^ (n - 1)
                    def Units.ofPowEqOne {M : Type u_1} [Monoid M] (a : M) (n : ) (ha : a ^ n = 1) (hn : n 0) :

                    If a ^ n = 1, n ≠ 0, then a is a unit.

                    Equations
                    Instances For
                      @[simp]
                      theorem AddUnits.nsmul_ofNSMulEqZero {M : Type u_1} [AddMonoid M] {n : } {a : M} (ha : n a = 0) (hn : n 0) :
                      @[simp]
                      theorem Units.pow_ofPowEqOne {M : Type u_1} [Monoid M] {n : } {a : M} (ha : a ^ n = 1) (hn : n 0) :
                      Units.ofPowEqOne a n ha hn ^ n = 1
                      theorem isAddUnit_ofNSMulEqZero {M : Type u_1} [AddMonoid M] {n : } {a : M} (ha : n a = 0) (hn : n 0) :
                      theorem isUnit_ofPowEqOne {M : Type u_1} [Monoid M] {n : } {a : M} (ha : a ^ n = 1) (hn : n 0) :
                      theorem AddCommute.sub_eq_sub_iff_of_isAddUnit {M : Type u_1} [SubtractionMonoid M] {a : M} {b : M} {c : M} {d : M} (hbd : AddCommute b d) (hb : IsAddUnit b) (hd : IsAddUnit d) :
                      a - b = c - d a + d = c + b
                      theorem Commute.div_eq_div_iff_of_isUnit {M : Type u_1} [DivisionMonoid M] {a : M} {b : M} {c : M} {d : M} (hbd : Commute b d) (hb : IsUnit b) (hd : IsUnit d) :
                      a / b = c / d a * d = c * b