English
For an injective RingHom f, CharP R p holds if and only if CharP A p holds.
Русский
Для инъективного RingHom f, CharP R p выполняется тогда и только тогда, когда CharP A p выполняется.
LaTeX
$$$( f ) \\; \\Rightarrow \\big( \\text{CharP}(R,p) \\iff \\text{CharP}(A,p) \\big)$$$
Lean4
/-- If `R →+* A` is injective, then `R` is of characteristic `p` if and only if `A` is also of
characteristic `p`. Similar to `RingHom.charZero_iff`. -/
protected theorem charP_iff {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A)
(H : Function.Injective f) (p : ℕ) : CharP R p ↔ CharP A p :=
⟨fun _ ↦ charP_of_injective_ringHom H p, fun _ ↦ f.charP H p⟩
