English
If f: R →+* A is injective, then ExpChar R p holds if and only if ExpChar A p holds.
Русский
Если f: R →+* A инъективен, то ExpChar R p выполняется тогда и только тогда, когда ExpChar A p выполняется.
LaTeX
$$$( f ) \\;\\Rightarrow \\big( \\operatorname{ExpChar}(R,p) \\iff \\operatorname{ExpChar}(A,p) \\big)$$$
Lean4
/-- If a ring homomorphism `R →+* A` is injective then `A` has the same exponential characteristic
as `R`. -/
theorem expChar_of_injective_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] {f : R →+* A}
(h : Function.Injective f) (q : ℕ) [hR : ExpChar R q] : ExpChar A q :=
by
rcases hR with _ | hprime
· haveI := charZero_of_injective_ringHom h; exact .zero
haveI := charP_of_injective_ringHom h q; exact .prime hprime
