subsemiring — Mathlib

English

If R has CharP p, then the Subring S inherits CharP p.

Русский

Если R имеет CharP p, то подкольцо S наследует CharP p.

LaTeX

$$$\\mathrm{CharP} S p$$$

Lean4

instance subsemiring (R : Type u) [Semiring R] (p : ℕ) [CharP R p] (S : Subsemiring R) : CharP S p :=
  ⟨fun x =>
    Iff.symm <|
      (CharP.cast_eq_zero_iff R p x).symm.trans
        ⟨fun h => Subtype.eq <| show S.subtype x = 0 by rw [map_natCast, h], fun h =>
          map_natCast S.subtype x ▸ by rw [h, RingHom.map_zero]⟩⟩

Похожие утверждения