Theorem: n1_2_26_ii' (AlgebraI/Subgroups.lean)

State before:
G : Type u_1
inst✝ : Group G
g h : G
⊢ ⁅g, h⁆ = 1 ↔ g * h = h * g
Tactic:
rw [commutatorElement_def, mul_inv_eq_iff_eq_mul, mul_inv_eq_iff_eq_mul, one_mul]
State after:
no goals