English
If R is a domain with CharP R p and f: R →+* A, then CharP A p.
Русский
Если R — домен и CharP R p, и есть кольцевое отображение f: R →+* A, тогда CharP A p.
LaTeX
$$$( \\text{CharP}(R,p) ) \\land (f : R \\to+* A) \\Rightarrow \\text{CharP}(A,p)$$$
Lean4
/-- Given `R →+* A`, where `R` is a domain with `char R > 0`, then `char A = char R`. -/
theorem of_ringHom_of_ne_zero {R A : Type*} [NonAssocSemiring R] [NoZeroDivisors R] [NonAssocSemiring A] [Nontrivial A]
(f : R →+* A) (p : ℕ) (hp : p ≠ 0) [CharP R p] : CharP A p :=
by
have := f.domain_nontrivial
have H := (CharP.char_is_prime_or_zero R p).resolve_right hp
obtain ⟨q, hq⟩ := CharP.exists A
obtain ⟨k, e⟩ := dvd_of_ringHom f p q
have := Nat.isUnit_iff.mp ((H.2 e).resolve_left (Nat.isUnit_iff.not.mpr (char_ne_one A q)))
rw [this, mul_one] at e
exact e ▸ hq
