HepLean Documentation

Mathlib.Algebra.Group.Commute.Units

Lemmas about commuting pairs of elements involving units. #

source
theorem AddCommute.addUnits_neg_right {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute a ↑u → AddCommute a ↑(-u)
source
theorem Commute.units_inv_right {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute a ↑u → Commute a ↑u⁻¹
source
@[simp]
theorem AddCommute.addUnits_neg_right_iff {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute a ↑(-u) ↔ AddCommute a ↑u
source
@[simp]
theorem Commute.units_inv_right_iff {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute a ↑u⁻¹ ↔ Commute a ↑u
source
theorem AddCommute.addUnits_neg_left {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute (↑u) a → AddCommute (↑(-u)) a
source
theorem Commute.units_inv_left {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute (↑u) a → Commute (↑u⁻¹) a
source
@[simp]
theorem AddCommute.addUnits_neg_left_iff {M : Type u_1} [AddMonoid M] {a : M} {u : AddUnits M} :
AddCommute (↑(-u)) a ↔ AddCommute (↑u) a
source
@[simp]
theorem Commute.units_inv_left_iff {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} :
Commute (↑u⁻¹) a ↔ Commute (↑u) a
source
theorem AddCommute.addUnits_val {M : Type u_1} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :
AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂
source
theorem Commute.units_val {M : Type u_1} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute u₁ u₂ → Commute ↑u₁ ↑u₂
source
theorem AddCommute.addUnits_of_val {M : Type u_1} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :
AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂
source
theorem Commute.units_of_val {M : Type u_1} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute ↑u₁ ↑u₂ → Commute u₁ u₂
source
@[simp]
theorem AddCommute.addUnits_val_iff {M : Type u_1} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :
AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂
source
@[simp]
theorem Commute.units_val_iff {M : Type u_1} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute ↑u₁ ↑u₂ ↔ Commute u₁ u₂
source
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
source
def AddUnits.leftOfAdd {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = ↑u) (hc : AddCommute a b) :
AddUnits M

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

Equations
  • u.leftOfAdd a b hu hc = { val := a, neg := b + ↑(-u), val_neg := ⋯, neg_val := ⋯ }
Instances For
    source
    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
    source
    def Units.leftOfMul {M : Type u_1} [Monoid M] (u : Mˣ) (a : M) (b : M) (hu : a * b = ↑u) (hc : Commute a b) :
    Mˣ

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

    Equations
    • u.leftOfMul a b hu hc = { val := a, inv := b * ↑u⁻¹, val_inv := ⋯, inv_val := ⋯ }
    Instances For
      source
      theorem AddUnits.rightOfAdd.proof_2 {M : Type u_1} [AddMonoid M] (a : M) (b : M) (hc : AddCommute a b) :
      AddCommute b a
      source
      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
      source
      def AddUnits.rightOfAdd {M : Type u_1} [AddMonoid M] (u : AddUnits M) (a : M) (b : M) (hu : a + b = ↑u) (hc : AddCommute a b) :
      AddUnits M

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

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

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

        Equations
        • u.rightOfMul a b hu hc = u.leftOfMul b a ⋯ ⋯
        Instances For
          source
          theorem AddCommute.isAddUnit_add_iff {M : Type u_1} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) :
          IsAddUnit (a + b) ↔ IsAddUnit a ∧ IsAddUnit b
          source
          theorem Commute.isUnit_mul_iff {M : Type u_1} [Monoid M] {a : M} {b : M} (h : Commute a b) :
          IsUnit (a * b) ↔ IsUnit a ∧ IsUnit b
          source
          @[simp]
          theorem isAddUnit_add_self_iff {M : Type u_1} [AddMonoid M] {a : M} :
          IsAddUnit (a + a) ↔ IsAddUnit a
          source
          @[simp]
          theorem isUnit_mul_self_iff {M : Type u_1} [Monoid M] {a : M} :
          IsUnit (a * a) ↔ IsUnit a
          source
          @[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)
          source
          @[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)
          source
          @[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
          source
          @[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
          source
          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
          source
          theorem AddUnits.ofNSMul.proof_2 {M : Type u_1} [AddMonoid M] (x : M) {n : ℕ} :
          AddCommute x ((n - 1) • x)
          source
          def AddUnits.ofNSMul {M : Type u_1} [AddMonoid M] (u : AddUnits M) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : n • x = ↑u) :
          AddUnits M

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

          Equations
          • u.ofNSMul x hn hu = u.leftOfAdd x ((n - 1) • x) ⋯ ⋯
          Instances For
            source
            def Units.ofPow {M : Type u_1} [Monoid M] (u : Mˣ) (x : M) {n : ℕ} (hn : n ≠ 0) (hu : x ^ n = ↑u) :
            Mˣ

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

            Equations
            • u.ofPow x hn hu = u.leftOfMul x (x ^ (n - 1)) ⋯ ⋯
            Instances For
              source
              @[simp]
              theorem isAddUnit_nsmul_iff {M : Type u_1} [AddMonoid M] {n : ℕ} {a : M} (hn : n ≠ 0) :
              IsAddUnit (n • a) ↔ IsAddUnit a
              source
              @[simp]
              theorem isUnit_pow_iff {M : Type u_1} [Monoid M] {n : ℕ} {a : M} (hn : n ≠ 0) :
              IsUnit (a ^ n) ↔ IsUnit a
              source
              theorem isAddUnit_nsmul_succ_iff {M : Type u_1} [AddMonoid M] {n : ℕ} {a : M} :
              IsAddUnit ((n + 1) • a) ↔ IsAddUnit a
              source
              theorem isUnit_pow_succ_iff {M : Type u_1} [Monoid M] {n : ℕ} {a : M} :
              IsUnit (a ^ (n + 1)) ↔ IsUnit a
              source
              def AddUnits.ofNSMulEqZero {M : Type u_1} [AddMonoid M] (a : M) (n : ℕ) (ha : n • a = 0) (hn : n ≠ 0) :
              AddUnits M

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

              Equations
              Instances For
                source
                @[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
                source
                @[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
                source
                @[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
                source
                @[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)
                source
                def Units.ofPowEqOne {M : Type u_1} [Monoid M] (a : M) (n : ℕ) (ha : a ^ n = 1) (hn : n ≠ 0) :
                Mˣ

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

                Equations
                Instances For
                  source
                  @[simp]
                  theorem AddUnits.nsmul_ofNSMulEqZero {M : Type u_1} [AddMonoid M] {n : ℕ} {a : M} (ha : n • a = 0) (hn : n ≠ 0) :
                  n • AddUnits.ofNSMulEqZero a n ha hn = 0
                  source
                  @[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
                  source
                  theorem isAddUnit_ofNSMulEqZero {M : Type u_1} [AddMonoid M] {n : ℕ} {a : M} (ha : n • a = 0) (hn : n ≠ 0) :
                  IsAddUnit a
                  source
                  theorem isUnit_ofPowEqOne {M : Type u_1} [Monoid M] {n : ℕ} {a : M} (ha : a ^ n = 1) (hn : n ≠ 0) :
                  IsUnit a
                  source
                  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
                  source
                  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