charP_of_injective_algebraMap' — Mathlib

English

If the algebra map R → A is injective and CharP R p, then 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

theorem charP_of_injective_algebraMap' (R A : Type*) [Field R] [Semiring A] [Algebra R A] [Nontrivial A] (p : ℕ)
    [CharP R p] : CharP A p :=
  charP_of_injective_algebraMap (algebraMap R A).injective p

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