English
Embedding is injective: (m : α) = (n : α) iff m = n.
Русский
Встраивание инъективно: (m : α) = (n : α) тогда и только тогда, когда m = n.
LaTeX
$$$$\forall {m,n : ZNum},\ (m : \alpha) = (n : \alpha) \iff m = n.$$$$
Lean4
@[simp, norm_cast]
theorem cast_inj [Ring α] [PartialOrder α] [IsStrictOrderedRing α] {m n : ZNum} : (m : α) = n ↔ m = n := by
rw [← cast_to_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]