Commute.inv_left
theorem Commute.inv_left : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → Commute a⁻¹ b
This theorem, called `Commute.inv_left`, states that for any type `G` that forms a group with a multiplication operation, if two elements `a` and `b` of `G` commute (meaning `a * b = b * a`), then the inverse of `a` also commutes with `b`. In other words, if `a` and `b` commute, then `a⁻¹ * b = b * a⁻¹` for any group `G`.
More concisely: If `a` and `b` are commuting elements of a group `G`, then their inverses also commute: `a⁻¹ * b = b * a⁻¹`.
|
Commute.inv_right
theorem Commute.inv_right : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → Commute a b⁻¹
This theorem, named 'Commute.inv_right', states that for any given type 'G' that is a group, with elements 'a' and 'b', if 'a' and 'b' commute (meaning the order of multiplication doesn't matter, i.e., `a * b = b * a`), then 'a' and the inverse of 'b' also commute. In other words, if `a * b = b * a`, it implies `a * b⁻¹ = b⁻¹ * a`.
More concisely: If `a` and `b` commute in group `G`, then `a` and the inverse of `b` also commute. That is, `a * b = b * a` implies `a * b⁻¹ = b⁻¹ * a`.
|