Characteristic of semirings of functions

instance CharP.pi (ι : Type u) [hi : Nonempty ι] (R : Type v) [Semiring R] (p : ℕ) [CharP R p] : CharP (ι → R) p

Equations

• (_ : CharP (ι → R) p) = (_ : CharP (ι → R) p)

instance CharP.pi' (ι : Type u) [Nonempty ι] (R : Type v) [CommRing R] (p : ℕ) [CharP R p] : CharP (ι → R) p

Equations

• (_ : CharP (ι → R) p) = (_ : CharP (ι → R) p)