cast_inj — Mathlib

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]

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