orderOf_eq_two_iff — Mathlib

English

If a group has exponent 2, then for any x, orderOf x = 2 iff x ≠ 1.

Русский

Если экспонента группы равна 2, то порядок элемента равен 2 тогда, когда x ≠ 1.

LaTeX

$$$\text{orderOf}(x) = 2 \iff x \neq 1$, given $\operatorname{exponent} G = 2$$$

Lean4

@[to_additive]
theorem orderOf_eq_two_iff (hG : Monoid.exponent G = 2) {x : G} : orderOf x = 2 ↔ x ≠ 1 :=
  ⟨by rintro hx rfl; norm_num at hx, orderOf_eq_prime (hG ▸ Monoid.pow_exponent_eq_one x)⟩

Похожие утверждения