charP_of_injective_algebraMap — Mathlib

English

If algebra map R → A is injective, CharP R p implies CharP A p.

Русский

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

LaTeX

$$$( \\text{CharP}(R,p) ) \\land (\\operatorname{algebraMap} R A) \\text{ injective } \\Rightarrow \\text{CharP}(A,p)$$$

Lean4

/-- If the algebra map `R →+* A` is injective then `A` has the same characteristic as `R`. -/
theorem charP_of_injective_algebraMap {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
    (h : Function.Injective (algebraMap R A)) (p : ℕ) [CharP R p] : CharP A p :=
  charP_of_injective_ringHom h p

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