castHom_bijective — Mathlib

English

Under the same hypotheses, ZMod.castHom is bijective.

Русский

При тех же условиях ZMod.castHom биективен.

LaTeX

$$$ \operatorname{Bijective} ( \operatorname{ZMod.castHom} (dvd\_refl n) \; R ) $$$

Lean4

theorem castHom_bijective [Fintype R] (h : Fintype.card R = n) : Function.Bijective (ZMod.castHom (dvd_refl n) R) :=
  by
  haveI : NeZero n :=
    ⟨by
      intro hn
      rw [hn] at h
      exact (Fintype.card_eq_zero_iff.mp h).elim' 0⟩
  rw [Fintype.bijective_iff_injective_and_card, ZMod.card, h, eq_self_iff_true, and_true]
  apply ZMod.castHom_injective

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