English
For a ring R of positive characteristic p and an additive character φ : R → R', each value φ(a) is a root of unity of order dividing p. Equivalently, (φ(a))^{p} = 1 in R'.
Русский
Для кольца R с положительной характеристикой p и аддитивной характеристики φ: R → R' каждое значение φ(a) является корнем единицы порядка, делящегося на p. Эквивалентно, (φ(a))^{p} = 1 в R'.
LaTeX
$$$(\phi(a))^{p} = 1\quad\text{where } p = \mathrm{char}(R)$$$
Lean4
/-- The values of an additive character on a ring of positive characteristic are roots of unity. -/
theorem val_mem_rootsOfUnity (φ : AddChar R R') (a : R) (h : 0 < ringChar R) :
(φ.val_isUnit a).unit ∈ rootsOfUnity (ringChar R).toPNat' R' := by
simp only [mem_rootsOfUnity', IsUnit.unit_spec, Nat.toPNat'_coe, h, ↓reduceIte, ← map_nsmul_eq_pow, nsmul_eq_mul,
CharP.cast_eq_zero, zero_mul, map_zero_eq_one]
