English
For an injective RingHom f, ExpChar R p holds if and only if ExpChar A p holds.
Русский
Для инъективного RingHom f, ExpChar R p выполняется тогда и только тогда, когда ExpChar A p выполняется.
LaTeX
$$$( f ) \\Rightarrow ( \\operatorname{ExpChar}(R,p) \\iff \\operatorname{ExpChar}(A,p) )$$$
Lean4
/-- If `R →+* A` is injective, then `R` is of exponential characteristic `p` if and only if `A` is
also of exponential characteristic `p`. Similar to `RingHom.charZero_iff`. -/
theorem expChar_iff {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (H : Function.Injective f)
(p : ℕ) : ExpChar R p ↔ ExpChar A p :=
⟨fun _ ↦ expChar_of_injective_ringHom H p, fun _ ↦ f.expChar H p⟩
