Lemmas about commuting pairs of elements involving units. #
theorem
AddCommute.addUnits_neg_right
{M : Type u_2}
[AddMonoid M]
{a : M}
{u : AddUnits M}
:
AddCommute a ↑u → AddCommute a ↑(-u)
@[simp]
theorem
AddCommute.addUnits_neg_right_iff
{M : Type u_2}
[AddMonoid M]
{a : M}
{u : AddUnits M}
:
AddCommute a ↑(-u) ↔ AddCommute a ↑u
theorem
AddCommute.addUnits_neg_left
{M : Type u_2}
[AddMonoid M]
{a : M}
{u : AddUnits M}
:
AddCommute (↑u) a → AddCommute (↑(-u)) a
@[simp]
theorem
AddCommute.addUnits_neg_left_iff
{M : Type u_2}
[AddMonoid M]
{a : M}
{u : AddUnits M}
:
AddCommute (↑(-u)) a ↔ AddCommute (↑u) a
theorem
AddCommute.addUnits_val
{M : Type u_2}
[AddMonoid M]
{u₁ : AddUnits M}
{u₂ : AddUnits M}
:
AddCommute u₁ u₂ → AddCommute ↑u₁ ↑u₂
theorem
AddCommute.addUnits_of_val
{M : Type u_2}
[AddMonoid M]
{u₁ : AddUnits M}
{u₂ : AddUnits M}
:
AddCommute ↑u₁ ↑u₂ → AddCommute u₁ u₂
@[simp]
theorem
AddCommute.addUnits_val_iff
{M : Type u_2}
[AddMonoid M]
{u₁ : AddUnits M}
{u₂ : AddUnits M}
:
AddCommute ↑u₁ ↑u₂ ↔ AddCommute u₁ u₂
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.
Instances For
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.
Instances For
theorem
AddUnits.rightOfAdd.proof_2
{M : Type u_1}
[AddMonoid M]
(a : M)
(b : M)
(hc : AddCommute a b)
:
AddCommute b a
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)
:
theorem
AddCommute.neg_right
{G : Type u_1}
[AddGroup G]
{a : G}
{b : G}
:
AddCommute a b → AddCommute a (-b)
@[simp]
theorem
AddCommute.neg_right_iff
{G : Type u_1}
[AddGroup G]
{a : G}
{b : G}
:
AddCommute a (-b) ↔ AddCommute a b
theorem
AddCommute.neg_left
{G : Type u_1}
[AddGroup G]
{a : G}
{b : G}
:
AddCommute a b → AddCommute (-a) b
@[simp]
theorem
AddCommute.neg_left_iff
{G : Type u_1}
[AddGroup G]
{a : G}
{b : G}
:
AddCommute (-a) b ↔ AddCommute a b
theorem
AddCommute.neg_add_cancel
{G : Type u_1}
[AddGroup G]
{a : G}
{b : G}
(h : AddCommute a b)
:
theorem
AddCommute.neg_add_cancel_assoc
{G : Type u_1}
[AddGroup G]
{a : G}
{b : G}
(h : AddCommute a b)
:
@[simp]
@[simp]