coe_toNNRat

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.coe_toNNRat

English

If q ≥ 0, then (q.toNNRat : ℚ) = q.

Русский

Если q ≥ 0, то (q.toNNRat : ℚ) = q.

LaTeX

$$$(q.toNNRat : \mathbb{Q}) = q \quad \text{for } q \ge 0$$$

Lean4

theorem _root_.Rat.coe_toNNRat (q : ℚ) (hq : 0 ≤ q) : (q.toNNRat : ℚ) = q :=
  max_eq_left hq

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

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

Разделы

Аффилиация

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