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) : ‖a‖ = 1

@[simp]

theorem AddChar.norm_apply {α : Type u_1} [NormedRing α] [NormMulClass α] [NormOneClass α] {G : Type u_3} [AddLeftCancelMonoid G] [Finite G] (ψ : AddChar G α) (x : G) : ‖ψ x‖ = 1