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 ↑u → AddCommute a ↑(-u)

theorem Commute.units_inv_right {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} : Commute a ↑u → Commute 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) a → AddCommute (↑(-u)) a

theorem Commute.units_inv_left {M : Type u_1} [Monoid M] {a : M} {u : Mˣ} : Commute (↑u) a → Commute (↑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) : AddUnits M

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

Equations

• AddUnits.leftOfAdd u a b hu hc = { val := a, neg := b + ↑(-u), val_neg := (_ : a + (b + ↑(-u)) = 0), neg_val := (_ : b + ↑(-u) + a = 0) }

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

• Units.leftOfMul u a b hu hc = { val := a, inv := b * ↑u⁻¹, val_inv := (_ : a * (b * ↑u⁻¹) = 1), inv_val := (_ : b * ↑u⁻¹ * a = 1) }

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) : AddCommute b a

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

• AddUnits.rightOfAdd u a b hu hc = AddUnits.leftOfAdd u b a (_ : b + a = ↑u) (_ : AddCommute b a)

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

• Units.rightOfMul u a b hu hc = Units.leftOfMul u b a (_ : b * a = ↑u) (_ : Commute b a)

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)

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

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

@[simp]

theorem isAddUnit_add_self_iff {M : Type u_1} [AddMonoid M] {a : M} : IsAddUnit (a + a) ↔ IsAddUnit a

@[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) : AddUnits M

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

Equations

• AddUnits.ofNSMul u x hn hu = AddUnits.leftOfAdd u x ((n - 1) • x) (_ : x + (n - 1) • x = ↑u) (_ : AddCommute x ((n - 1) • x))

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) : Mˣ

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

Equations

• Units.ofPow u x hn hu = Units.leftOfMul u x (x ^ (n - 1)) (_ : x * x ^ (n - 1) = ↑u) (_ : Commute x (x ^ (n - 1)))

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)

@[simp]

theorem isAddUnit_nsmul_iff {M : Type u_1} [AddMonoid M] {n : ℕ} {a : M} (hn : n ≠ 0) : IsAddUnit (n • a) ↔ IsAddUnit a

@[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} : IsAddUnit ((n + 1) • a) ↔ IsAddUnit a

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) : AddUnits M

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

Equations

• AddUnits.ofNSMulEqZero a n ha hn = AddUnits.ofNSMul 0 a hn ha

@[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) : Mˣ

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

Equations

• Units.ofPowEqOne a n ha hn = Units.ofPow 1 a hn ha

@[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

@[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) : IsAddUnit a

theorem isUnit_ofPowEqOne {M : Type u_1} [Monoid M] {n : ℕ} {a : M} (ha : a ^ n = 1) (hn : n ≠ 0) : IsUnit a

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