isUnit_unit — Mathlib

English

If ζ is a primitive n-th root of unity in a commutative monoid and ζ is a unit, then the corresponding unit element is also a primitive n-th root of unity.

Русский

Пусть ζ — примитивный корень порядка n в коммутативном моноиде и ζ является единицей; тогда соответствующий элемент в группе единиц также является примитивным корнем порядка n.

LaTeX

$$$$\text{If } \zeta \text{ is a primitive } n\text{-th root of unity and } \zeta \text{ is invertible, then the corresponding unit yields a primitive } n\text{-th root of unity.}$$$$

Lean4

theorem isUnit_unit {ζ : M} {n} (hn) (hζ : IsPrimitiveRoot ζ n) : IsPrimitiveRoot (hζ.isUnit hn).unit n :=
  coe_units_iff.mp hζ

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