cast_zmod_eq_zero_iff_of_le — Mathlib

English

For m ≤ n and a ∈ ZMod m with NeZero m, (cast a : ZMod n) = 0 iff a = 0.

Русский

Для m ≤ n и a ∈ ZMod m с NeZero m, (cast a : ZMod n) = 0 тогда и только тогда a = 0.

LaTeX

$$$\forall m,n\ [NeZero m]\ (h:m\le n)\ (a:ZMod m),\ cast(a) = 0 \iff a = 0$$$

Lean4

theorem cast_zmod_eq_zero_iff_of_le {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ZMod m) : (cast a : ZMod n) = 0 ↔ a = 0 :=
  by
  rw [← ZMod.cast_zero (n := m)]
  exact Injective.eq_iff' (cast_injective_of_le h) rfl

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