natCast_eq_divNat

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.natCast_eq_divNat

English

For every natural number n, the natural cast to NRat equals divNat(n,1).

Русский

Для каждого натурального числа n, его привод к NRat равен divNat(n,1).

LaTeX

$$$ (n : \mathbb{Q}_{\ge 0}) = \mathrm{divNat}(n,1) $$$

Lean4

theorem natCast_eq_divNat (n : ℕ) : (n : ℚ≥0) = divNat n 1 :=
  (num_divNat_den _).symm

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

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

Разделы

Аффилиация

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