cast_eq_zero — Mathlib

English

The cast from integers to α is injective: if m.cast = n.cast then m = n.

Русский

Приведение из целых чисел в α инъективно: если m.cast = n.cast, то m = n.

LaTeX

$$$ \forall {\alpha} [AddGroupWithOne \alpha] [CharZero \alpha],\ (m,n : \mathbb{Z}),\ (m : \alpha) = (n : \alpha) \Rightarrow m = n.$$$

Lean4

@[simp]
theorem cast_eq_zero : (n : α) = 0 ↔ n = 0
    where
  mp
    h := by
    cases n
    · rw [ofNat_eq_coe, Int.cast_natCast] at h
      exact congr_arg _ (Nat.cast_eq_zero.1 h)
    · rw [cast_negSucc, neg_eq_zero, Nat.cast_eq_zero] at h
      contradiction
  mpr h := by rw [h, cast_zero]

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