toNNRat_coe

Mathlib.Data.NNRat.Defs

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

English

For every q in ℚ≥0, toNNRat q = q.

Русский

Для каждого q в ℚ≥0 верно toNNRat q = q.

LaTeX

$$$$ \mathrm{toNNRat}(q) = q \quad\text{for all } q \in \mathbb{Q}_{\ge 0}. $$$$

Lean4

@[simp]
theorem toNNRat_coe (q : ℚ≥0) : toNNRat q = q :=
  ext <| max_eq_left q.2

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

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

Разделы

Аффилиация

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