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
/-- If `R →+* A` is injective, and `A` is of exponential characteristic `p`, then `R` is also of
exponential characteristic `p`. Similar to `RingHom.charZero`. -/
theorem expChar {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f) (p : ℕ)
[ExpChar A p] : ExpChar R p := by
cases ‹ExpChar A p› with
| zero => haveI := f.charZero; exact .zero
| prime hp => haveI := f.charP H p; exact .prime hp
