cast_inj

Mathlib.Algebra.CharZero.Defs

URI: https://scilib.ai/kg/mathlib#Nat.cast_inj

English

For all m,n ∈ ℕ, (m : R) = (n : R) iff m = n.

Русский

Для любых m,n ∈ ℕ, (m в R) = (n в R) эквивалентно m = n.

LaTeX

$$∀ {m n : ℕ}, (m : R) = (n : R) \\\\iff m = n$$

Lean4

@[simp, norm_cast]
theorem cast_inj {m n : ℕ} : (m : R) = n ↔ m = n :=
  cast_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru