Finite order elements in normed rings. #
A finite order element in a normed ring has norm 1.
The values of additive characters on finite cancellative monoids have norm 1.
theorem
IsOfFinOrder.norm_eq_one
{α : Type u_1}
[NormedRing α]
[NormMulClass α]
[NormOneClass α]
{a : α}
(ha : IsOfFinOrder a)
:
@[simp]
theorem
AddChar.norm_apply
{α : Type u_1}
[NormedRing α]
[NormMulClass α]
[NormOneClass α]
{G : Type u_3}
[AddLeftCancelMonoid G]
[Finite G]
(ψ : AddChar G α)
(x : G)
: