ringHom_surjective — Mathlib

English

Any ring homomorphism from any nonassociative ring R into ZMod n is surjective.

Русский

Любой кольцевой гомоморфизм из любого неассоциативного кольца R в ZMod n является сюръективным.

LaTeX

$$$\text{Surjective } (f : R \to+* ZMod\ n)$$$

Lean4

/-- Any ring homomorphism into `ZMod n` is surjective. -/
theorem ringHom_surjective [NonAssocRing R] (f : R →+* ZMod n) : Function.Surjective f :=
  (ringHom_rightInverse f).surjective

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