English
If 0 < n, then the rotation r by one step has order n; i.e., the rotation r(1) generates the cyclic subgroup of size n.
Русский
Если 0 < n, то вращение r единичного шага имеет порядок n; т.е. вращение r(1) порождает циклическую подгруппу размера n.
LaTeX
$$$\operatorname{order}(r(1)) = n$$$
Lean4
/-- If `0 < n`, then `r 1` has order `n`.
-/
@[simp]
theorem orderOf_r_one : orderOf (r 1 : DihedralGroup n) = n :=
by
rcases eq_zero_or_neZero n with (rfl | hn)
· rw [orderOf_eq_zero_iff']
intro n hn
rw [r_one_pow, one_def]
apply mt r.inj
simpa using hn.ne'
· apply (Nat.le_of_dvd (NeZero.pos n) <| orderOf_dvd_of_pow_eq_one <| @r_one_pow_n n).lt_or_eq.resolve_left
intro h
have h1 : (r 1 : DihedralGroup n) ^ orderOf (r 1) = 1 := pow_orderOf_eq_one _
rw [r_one_pow] at h1
injection h1 with h2
rw [← ZMod.val_eq_zero, ZMod.val_natCast, Nat.mod_eq_of_lt h] at h2
exact absurd h2.symm (orderOf_pos _).ne
