English
The character p passes to function spaces: if R has characteristic p, then the function space ι → R also has characteristic p.
Русский
Если у R характеристика p, то пространство функций ι → R имеет характеристику p.
LaTeX
$$$\\operatorname{CharP}(\\iota \\to R)\\; p$ при |CharP(R,p)|$$
Lean4
instance pi (ι : Type u) [hi : Nonempty ι] (R : Type v) [Semiring R] (p : ℕ) [CharP R p] : CharP (ι → R) p :=
⟨fun x =>
let ⟨i⟩ := hi
Iff.symm <|
(CharP.cast_eq_zero_iff R p x).symm.trans
⟨fun h => funext fun j => show Pi.evalRingHom (fun _ => R) j (↑x : ι → R) = 0 by rw [map_natCast, h], fun h =>
map_natCast (Pi.evalRingHom (fun _ : ι => R) i) x ▸ by rw [h, RingHom.map_zero]⟩⟩
-- diamonds
