English
If f: R →+* A is injective, then CharP R p holds if and only if CharP A p holds.
Русский
Если f: R →+* A инъективен, то CharP R p выполняется тогда и только тогда, когда CharP A p выполняется.
LaTeX
$$$( f : R \\to+* A ) \\text{ injective } \\Rightarrow ( \\text{CharP}(R,p) \\iff \\text{CharP}(A,p) )$$$
Lean4
/-- If `R →+* A` is injective, and `A` is of characteristic `p`, then `R` is also of
characteristic `p`. Similar to `RingHom.charZero`. -/
theorem charP {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ℕ)
[CharP A p] : CharP R p := by
obtain ⟨q, h⟩ := CharP.exists R
exact CharP.eq _ (charP_of_injective_ringHom H q) ‹CharP A p› ▸ h
