Lemmas about commuting pairs of elements involving units. #

source

theorem AddCommute.addUnits_neg_right {M : Type u_2} [AddMonoid M] {a : M} {u : AddUnits M} :

AddCommute a ↑u → AddCommute a ↑(-u)

source

theorem Commute.units_inv_right {M : Type u_2} [Monoid M] {a : M} {u : Mˣ} :

Commute a ↑u → Commute a ↑u⁻¹

source

@[simp]

theorem AddCommute.addUnits_neg_right_iff {M : Type u_2} [AddMonoid M] {a : M} {u : AddUnits M} :

AddCommute a ↑(-u) ↔ AddCommute a ↑u

source

@[simp]

theorem Commute.units_inv_right_iff {M : Type u_2} [Monoid M] {a : M} {u : Mˣ} :

Commute a ↑u⁻¹ ↔ Commute a ↑u

source

theorem AddCommute.addUnits_neg_left {M : Type u_2} [AddMonoid M] {a : M} {u : AddUnits M} :

AddCommute (↑u) a → AddCommute (↑(-u)) a

source

theorem Commute.units_inv_left {M : Type u_2} [Monoid M] {a : M} {u : Mˣ} :

Commute (↑u) a → Commute (↑u⁻¹) a

source

@[simp]

theorem AddCommute.addUnits_neg_left_iff {M : Type u_2} [AddMonoid M] {a : M} {u : AddUnits M} :

AddCommute (↑(-u)) a ↔ AddCommute (↑u) a

source

@[simp]

theorem Commute.units_inv_left_iff {M : Type u_2} [Monoid M] {a : M} {u : Mˣ} :

Commute (↑u⁻¹) a ↔ Commute (↑u) a

source

theorem AddCommute.addUnits_val {M : Type u_2} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :

AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂

source

theorem Commute.units_val {M : Type u_2} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :

Commute u₁ u₂ → Commute ↑u₁ ↑u₂

source

theorem AddCommute.addUnits_of_val {M : Type u_2} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :

AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂

source

theorem Commute.units_of_val {M : Type u_2} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :

Commute ↑u₁ ↑u₂ → Commute u₁ u₂

source

@[simp]

theorem AddCommute.addUnits_val_iff {M : Type u_2} [AddMonoid M] {u₁ : AddUnits M} {u₂ : AddUnits M} :

AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂

source

@[simp]

theorem Commute.units_val_iff {M : Type u_2} [Monoid M] {u₁ : Mˣ} {u₂ : Mˣ} :

Commute ↑u₁ ↑u₂ ↔ Commute u₁ u₂

source

def AddUnits.leftOfAdd {M : Type u_2} [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) }

Instances For

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

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_2} [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) }

Instances For

source

def AddUnits.rightOfAdd {M : Type u_2} [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)

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 Units.rightOfMul {M : Type u_2} [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)

Instances For

source

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, ↑u = a + b)) → motive x

Equations

AddCommute.isAddUnit_add_iff.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

source

theorem AddCommute.isAddUnit_add_iff {M : Type u_2} [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_2} [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_2} [AddMonoid M] {a : M} :

IsAddUnit (a + a) ↔ IsAddUnit a

source

@[simp]

theorem isUnit_mul_self_iff {M : Type u_2} [Monoid M] {a : M} :

IsUnit (a * a) ↔ IsUnit a

source

theorem AddCommute.neg_right {G : Type u_1} [AddGroup G] {a : G} {b : G} :

AddCommute a b → AddCommute a (-b)

source

theorem Commute.inv_right {G : Type u_1} [Group G] {a : G} {b : G} :

Commute a b → Commute a b⁻¹

source

@[simp]

theorem AddCommute.neg_right_iff {G : Type u_1} [AddGroup G] {a : G} {b : G} :

AddCommute a (-b) ↔ AddCommute a b

source

@[simp]

theorem Commute.inv_right_iff {G : Type u_1} [Group G] {a : G} {b : G} :

Commute a b⁻¹ ↔ Commute a b

source

theorem AddCommute.neg_left {G : Type u_1} [AddGroup G] {a : G} {b : G} :

AddCommute a b → AddCommute (-a) b

source

theorem Commute.inv_left {G : Type u_1} [Group G] {a : G} {b : G} :

Commute a b → Commute a⁻¹ b

source

@[simp]

theorem AddCommute.neg_left_iff {G : Type u_1} [AddGroup G] {a : G} {b : G} :

AddCommute (-a) b ↔ AddCommute a b

source

@[simp]

theorem Commute.inv_left_iff {G : Type u_1} [Group G] {a : G} {b : G} :

Commute a⁻¹ b ↔ Commute a b

source

theorem AddCommute.neg_add_cancel {G : Type u_1} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) :

-a + b + a = b

source

theorem Commute.inv_mul_cancel {G : Type u_1} [Group G] {a : G} {b : G} (h : Commute a b) :

a⁻¹ * b * a = b

source

theorem AddCommute.neg_add_cancel_assoc {G : Type u_1} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) :

-a + (b + a) = b

source

theorem Commute.inv_mul_cancel_assoc {G : Type u_1} [Group G] {a : G} {b : G} (h : Commute a b) :

a⁻¹ * (b * a) = b

source

@[simp]

theorem neg_add_cancel_comm {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :

-a + b + a = b

source

@[simp]

theorem inv_mul_cancel_comm {G : Type u_1} [CommGroup G] (a : G) (b : G) :

a⁻¹ * b * a = b

source

@[simp]

theorem neg_add_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :

-a + (b + a) = b

source

@[simp]

theorem inv_mul_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a : G) (b : G) :

a⁻¹ * (b * a) = b