charZero_of_injective_ringHom — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If a ring homomorphism `R →+* A` is injective and `R` has characteristic zero
then so does `A`. -/
theorem charZero_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A}
    (h : Function.Injective f) [CharZero R] : CharZero A where
  cast_injective _ _ _ := CharZero.cast_injective <| h <| by simpa only [map_natCast f]

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