ofNat_eq_ofNat

Mathlib.Algebra.CharZero.Defs

URI: https://scilib.ai/kg/mathlib#OfNat.ofNat_eq_ofNat

English

If m,n ≥ 2, then (ofNat m : R) = ofNat n in R holds iff m = n.

Русский

Пусть m,n ≥ 2. Тогда (ofNat m : R) = ofNat n в R эквивалентно m = n.

LaTeX

$$$ (m : R) = (n : R) \iff m = n \quad\text{for } m,n \ge 2 $$$

Lean4

@[simp]
theorem ofNat_eq_ofNat {m n : ℕ} [m.AtLeastTwo] [n.AtLeastTwo] : (ofNat(m) : R) = ofNat(n) ↔ (ofNat m : ℕ) = ofNat n :=
  Nat.cast_inj

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

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

Разделы

Аффилиация

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