charP_of_injective_ringHom — Mathlib

English

If a ring homomorphism f: R →+* A is injective and CharP R p, then CharP A p.

Русский

Если отображение f: R →+* A инъективно и CharP R p, то CharP A p.

LaTeX

$$$( \\text{CharP}(R,p) ) \\land ( f : R \\to+* A ) \\Rightarrow \\text{CharP}(A,p)$$$

Lean4

/-- If a ring homomorphism `R →+* A` is injective then `A` has the same characteristic as `R`. -/
theorem charP_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A}
    (h : Function.Injective f) (p : ℕ) [CharP R p] : CharP A p where
  cast_eq_zero_iff x := by rw [← CharP.cast_eq_zero_iff R p x, ← map_natCast f x, map_eq_zero_iff f h]

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