mathlib3 documentation

algebra.char_p.pi

Characteristic of semirings of functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, instance]
def char_p.pi (ι : Type u) [hi : nonempty ι] (R : Type v) [semiring R] (p : ℕ) [char_p R p] :
char_p (ι → R) p
source
@[protected, instance]
def char_p.pi' (ι : Type u) [hi : nonempty ι] (R : Type v) [comm_ring R] (p : ℕ) [char_p R p] :
char_p (ι → R) p