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

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯