charZero_of_injective_algebraMap — Mathlib

English

If the algebra map R → A is injective and CharZero R, then CharZero A.

Русский

Если алгебраическая карта R → A инъективна и CharZero R, то CharZero A.

LaTeX

$$$( \\text{CharZero}(R) ) \\land (\\operatorname{algebraMap} R A) \\text{ injective } \\Rightarrow \\text{CharZero}(A)$$$

Lean4

/-- If the algebra map `R →+* A` is injective and `R` has characteristic zero then so does `A`. -/
theorem charZero_of_injective_algebraMap {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (h : Function.Injective (algebraMap R A)) [CharZero R] : CharZero A :=
  charZero_of_injective_ringHom h

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