toNNRat_eq_zero

Mathlib.Data.NNRat.Defs

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

English

For p,q ∈ ℚ≥0, p − q equals toNNRat(p − q).

Русский

Для p,q ∈ ℚ≥0, p − q равняется toNNRat(p − q).

LaTeX

$$$p - q = \operatorname{toNNRat}(p - q)\quad(p,q \in \mathbb{Q}_{\ge 0}).$$$

Lean4

@[simp]
theorem toNNRat_eq_zero : toNNRat q = 0 ↔ q ≤ 0 := by simpa [-toNNRat_pos] using (@toNNRat_pos q).not

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

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

Разделы

Аффилиация

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