English
If every element has order dividing 2 in a cancellative monoid, then any two elements commute.
Русский
Если каждый элемент имеет порядок делимый на 2 в перестановочном монаде, тогда любые два элемента commute.
LaTeX
$$$[IsCancelMul\ G] \Rightarrow (\forall a,b\, (orderOf(a) \mid 2) \rightarrow (orderOf(b) \mid 2) \rightarrow ab=ba)$$$
Lean4
@[to_additive]
theorem of_orderOf_dvd_two [IsCancelMul G] (h : ∀ g : G, orderOf g ∣ 2) (a b : G) : Commute a b :=
by
simp_rw [orderOf_dvd_iff_pow_eq_one] at h
rw [commute_iff_eq, ← mul_right_inj a, ← mul_left_inj b]
-- We avoid `group` here to minimize imports while low in the hierarchy;
-- typically it would be better to invoke the tactic.
calc
a * (a * b) * b = a ^ 2 * b ^ 2 := by simp [pow_two, mul_assoc]
_ = 1 := by rw [h, h, mul_one]
_ = (a * b) ^ 2 := by rw [h]
_ = a * (b * a) * b := by simp [pow_two, mul_assoc]
