castHom_surjective — Mathlib

English

If h divides n, the canonical castHom from ZMod n to ZMod m is surjective.

Русский

Если h делит n, канонический castHom из ZMod n в ZMod m сюръективен.

LaTeX

$$$\\\\forall h : m \\\\mid n, \\\\operatorname{castHom} h (ZMod m) : ZMod n \\\\to+* ZMod m \\\\text{ is surjective}$$$

Lean4

theorem castHom_surjective (h : m ∣ n) : Function.Surjective (castHom h (ZMod m)) := fun a ↦ by
  obtain ⟨a, rfl⟩ := intCast_surjective a; exact ⟨a, map_intCast ..⟩

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