# Lemmas about commuting pairs of elements involving units. #

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

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

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
theorem AddUnits.rightOfAdd.proof_2 {M : Type u_1} [] (a : M) (b : M) (hc : ) :
theorem AddUnits.rightOfAdd.proof_1 {M : Type u_1} [] (u : ) (a : M) (b : M) (hu : a + b = u) (hc : ) :
b + a = u
def Units.rightOfMul {M : Type u_1} [] (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
• u.rightOfMul a b hu hc = u.leftOfMul b a
Instances For
abbrev AddCommute.isAddUnit_add_iff.match_1 {M : Type u_1} [] {a : M} {b : M} (motive : IsAddUnit (a + b)Prop) :
∀ (x : IsAddUnit (a + b)), (∀ (u : ) (hu : u = a + b), motive )motive x
Equations
• =
Instances For
theorem AddCommute.isAddUnit_add_iff {M : Type u_1} [] {a : M} {b : M} (h : ) :
IsAddUnit (a + b)
theorem Commute.isUnit_mul_iff {M : Type u_1} [] {a : M} {b : M} (h : Commute a b) :
IsUnit (a * b)
@[simp]
theorem isAddUnit_add_self_iff {M : Type u_1} [] {a : M} :
IsAddUnit (a + a)
@[simp]
theorem isUnit_mul_self_iff {M : Type u_1} [] {a : M} :
IsUnit (a * a)
@[simp]
theorem AddCommute.addUnits_zsmul_right {M : Type u_1} [] {a : M} {u : } (h : AddCommute a u) (m : ) :
AddCommute a (m u)
@[simp]
theorem Commute.units_zpow_right {M : Type u_1} [] {a : M} {u : Mˣ} (h : Commute a u) (m : ) :
Commute a (u ^ m)
@[simp]
theorem AddCommute.addUnits_zsmul_left {M : Type u_1} [] {a : M} {u : } (h : AddCommute (u) a) (m : ) :
AddCommute ((m u)) a
@[simp]
theorem Commute.units_zpow_left {M : Type u_1} [] {a : M} {u : Mˣ} (h : Commute (u) a) (m : ) :
Commute ((u ^ m)) a
theorem AddUnits.ofNSMul.proof_2 {M : Type u_1} [] (x : M) {n : } :
AddCommute x ((n - 1) x)
def AddUnits.ofNSMul {M : Type u_1} [] (u : ) (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
• u.ofNSMul x hn hu = u.leftOfAdd x ((n - 1) x)
Instances For
theorem AddUnits.ofNSMul.proof_1 {M : Type u_1} [] (u : ) (x : M) {n : } (hn : n 0) (hu : n x = u) :
x + (n - 1) x = u
def Units.ofPow {M : Type u_1} [] (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
• u.ofPow x hn hu = u.leftOfMul x (x ^ (n - 1))
Instances For
abbrev isAddUnit_nsmul_iff.match_1 {M : Type u_1} [] {n : } {a : M} (motive : IsAddUnit (n a)Prop) :
∀ (x : IsAddUnit (n a)), (∀ (u : ) (hu : u = n a), motive )motive x
Equations
• =
Instances For
@[simp]
theorem isAddUnit_nsmul_iff {M : Type u_1} [] {n : } {a : M} (hn : n 0) :
@[simp]
theorem isUnit_pow_iff {M : Type u_1} [] {n : } {a : M} (hn : n 0) :
IsUnit (a ^ n)
theorem isAddUnit_nsmul_succ_iff {M : Type u_1} [] {n : } {a : M} :
IsAddUnit ((n + 1) a)
theorem isUnit_pow_succ_iff {M : Type u_1} [] {n : } {a : M} :
IsUnit (a ^ (n + 1))
def AddUnits.ofNSMulEqZero {M : Type u_1} [] (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} [] (a : M) (n : ) (ha : n a = 0) (hn : n 0) :
(-AddUnits.ofNSMulEqZero a n ha hn) = (n - 1) a
@[simp]
theorem Units.val_inv_ofPowEqOne {M : Type u_1} [] (a : M) (n : ) (ha : a ^ n = 1) (hn : n 0) :
(Units.ofPowEqOne a n ha hn)⁻¹ = a ^ (n - 1)
@[simp]
theorem Units.val_ofPowEqOne {M : Type u_1} [] (a : M) (n : ) (ha : a ^ n = 1) (hn : n 0) :
(Units.ofPowEqOne a n ha hn) = a
@[simp]
theorem AddUnits.val_ofNSMulEqZero {M : Type u_1} [] (a : M) (n : ) (ha : n a = 0) (hn : n 0) :
(AddUnits.ofNSMulEqZero a n ha hn) = a
def Units.ofPowEqOne {M : Type u_1} [] (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} [] {n : } {a : M} (ha : n a = 0) (hn : n 0) :
@[simp]
theorem Units.pow_ofPowEqOne {M : Type u_1} [] {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} [] {n : } {a : M} (ha : n a = 0) (hn : n 0) :
theorem isUnit_ofPowEqOne {M : Type u_1} [] {n : } {a : M} (ha : a ^ n = 1) (hn : n 0) :
theorem AddCommute.sub_eq_sub_iff_of_isAddUnit {M : Type u_1} {a : M} {b : M} {c : M} {d : M} (hbd : ) (hb : ) (hd : ) :
a - b = c - d a + d = c + b
theorem Commute.div_eq_div_iff_of_isUnit {M : Type u_1} [] {a : M} {b : M} {c : M} {d : M} (hbd : Commute b d) (hb : ) (hd : ) :
a / b = c / d a * d = c * b