Characteristic of semirings of functions

theorem CharZero.pi {ι : Type u_1} {α : ι → Type u_2} (i : ι) [(i : ι) → AddMonoidWithOne (α i)] [CharZero (α i)] : CharZero ((i : ι) → α i)

instance Pi.instCharZero {ι : Type u_1} {α : ι → Type u_2} [Nonempty ι] [(i : ι) → AddMonoidWithOne (α i)] [∀ (i : ι), CharZero (α i)] : CharZero ((i : ι) → α i)

Strictly this only needs any one component to be char-zero, but this is awkward to express.

instance Pi.instCharP {ι : Type u_1} {α : ι → Type u_2} [Nonempty ι] [(i : ι) → AddMonoidWithOne (α i)] (p : ℕ) [∀ (i : ι), CharP (α i) p] : CharP ((i : ι) → α i) p

instance Pi.instExpChar {ι : Type u_1} {α : ι → Type u_2} [Nonempty ι] [(i : ι) → AddMonoidWithOne (α i)] (p : ℕ) [∀ (i : ι), ExpChar (α i) p] : ExpChar ((i : ι) → α i) p