mathlib3 documentation

algebra.char_p.subring

Characteristic of subrings #

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

source
@[protected, instance]
def char_p.subsemiring (R : Type u) [semiring R] (p : ℕ) [char_p R p] (S : subsemiring R) :
char_p ↥S p
source
@[protected, instance]
def char_p.subring (R : Type u) [ring R] (p : ℕ) [char_p R p] (S : subring R) :
char_p ↥S p
source
@[protected, instance]
def char_p.subring' (R : Type u) [comm_ring R] (p : ℕ) [char_p R p] (S : subring R) :
char_p ↥S p