English
The set of k-th roots of unity in a commutative monoid M is the subgroup of Mˣ consisting of elements ζ with ζ^k = 1.
Русский
Множество k-й корней единства в коммутативном моноиде M образует подгруппу Mˣ consisting of ζ with ζ^k = 1.
LaTeX
$$$\mathrm{rootsOfUnity}(k,M) = \{\zeta \in M^{\times} \mid \zeta^{k} = 1\}$$$
Lean4
/-- `rootsOfUnity k M` is the subgroup of elements `m : Mˣ` that satisfy `m ^ k = 1`. -/
def rootsOfUnity (k : ℕ) (M : Type*) [CommMonoid M] : Subgroup Mˣ
where
carrier := {ζ | ζ ^ k = 1}
one_mem' := one_pow _
mul_mem' _ _ := by simp_all only [Set.mem_setOf_eq, mul_pow, one_mul]
inv_mem' _ := by simp_all only [Set.mem_setOf_eq, inv_pow, inv_one]
