toNNRat_coe_nat

Mathlib.Data.NNRat.Defs

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

English

The natural embedding commutes with toNNRat: for every natural n, toNNRat n = n.

Русский

Естественное вложение согласуется с toNNRat: для каждого натурального n, toNNRat n = n.

LaTeX

$$$$ \mathrm{toNNRat}(n) = n \quad\text{for all } n \in \mathbb{N}. $$$$

Lean4

@[simp]
theorem toNNRat_coe_nat (n : ℕ) : toNNRat n = n :=
  ext <| by simp only [Nat.cast_nonneg', Rat.coe_toNNRat]; rfl

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

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

Разделы

Аффилиация

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