English
If the algebra map R →+* A is injective, then ExpChar R p holds if ExpChar A p holds.
Русский
Если отображение R →+* A инъективно, то ExpChar R p выполняется при ExpChar A p.
LaTeX
$$$( \\operatorname{algebraMap} R A ) \\text{ injective } \\Rightarrow ( \\operatorname{ExpChar}(R,p) \\iff \\operatorname{ExpChar}(A,p) )$$$
Lean4
/-- A nontrivial `ℚ`-algebra has `CharP` equal to zero.
This cannot be a (local) instance because it would immediately form a loop with the
instance `DivisionRing.toRatAlgebra`. It's probably easier to go the other way: prove `CharZero R`
and automatically receive an `Algebra ℚ R` instance.
-/
theorem charP_zero [Semiring R] [Algebra ℚ R] : CharP R 0 :=
charP_of_injective_algebraMap (algebraMap ℚ R).injective 0
