num_ne_zero

Mathlib.Data.NNRat.Defs

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

English

For q ∈ ℚ≥0, q.num ≠ 0 if and only if q ≠ 0.

Русский

Для q ∈ ℚ≥0 верно: q.num ≠ 0 ⇔ q ≠ 0.

LaTeX

$$$ q.num \neq 0 \iff q \neq 0 $$$

Lean4

@[simp]
theorem num_ne_zero : q.num ≠ 0 ↔ q ≠ 0 := by simp [num]

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

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

Разделы

Аффилиация

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