cast_inj — Mathlib

English

If casts to α agree and α has characteristic zero, then the original PosNum are equal.

Русский

Если два PosNum при приведении в α дают одинаковые значения и α имеет характеристику ноль, то эти PosNum равны.

LaTeX

$$$[AddMonoidWithOne \\alpha] [CharZero \\alpha] \\{m,n : \\text{PosNum}\\} : (m : \\alpha) = (n : \\alpha) \\iff m = n$$$

Lean4

@[simp, norm_cast]
theorem cast_inj [AddMonoidWithOne α] [CharZero α] {m n : PosNum} : (m : α) = n ↔ m = n := by
  rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]

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