dvd_of_ringHom — Mathlib

English

For any ring homomorphism f: R →+* A between nonassoc semirings, if CharP R p and CharP A q, then q divides p.

Русский

Для кольцевого однородного отображения f: R →+* A между неассоциативными полукольцами, если CharP R p и CharP A q, тогда q делит p.

LaTeX

$$$( \\text{CharP}(R,p) ) \\land ( \\text{CharP}(A,q) ) \\land (f : R \\to+* A) \\Rightarrow (q \\mid p)$$$

Lean4

/-- Given `R →+* A`, then `char A ∣ char R`. -/
theorem dvd_of_ringHom {R A : Type*} [NonAssocSemiring R] [NonAssocSemiring A] (f : R →+* A) (p q : ℕ) [CharP R p]
    [CharP A q] : q ∣ p := by
  refine (CharP.cast_eq_zero_iff A q p).mp ?_
  rw [← map_natCast f p, CharP.cast_eq_zero, map_zero]

Похожие утверждения