castHom_injective — Mathlib

English

If R is finite with card R = n and CharP R n, then the canonical map ZMod n → R is injective.

Русский

Если R конечное сcard(R) = n и CharP R n, то каноническое отображение ZMod n → R инъективно.

LaTeX

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

Lean4

theorem castHom_injective : Function.Injective (ZMod.castHom (dvd_refl n) R) :=
  by
  rw [injective_iff_map_eq_zero]
  intro x
  obtain ⟨k, rfl⟩ := ZMod.intCast_surjective x
  rw [map_intCast, CharP.intCast_eq_zero_iff R n, CharP.intCast_eq_zero_iff (ZMod n) n]
  exact id

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