mkRat_nonneg_iff

Mathlib.Algebra.Order.Ring.Unbundled.Rat

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

← MathLib Explorer

English

For integer a and positive denominator, 0 ≤ mkRat a b iff 0 ≤ a.

Русский

Для целого a и положительного знаменателя 0 ≤ mkRat a b эквивалентно 0 ≤ a.

LaTeX

$$$$0 \\le mkRat\\ (a)\\ b \\iff 0 \\le a.$$$$

Lean4

theorem mkRat_nonneg_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : 0 ≤ mkRat a b ↔ 0 ≤ a :=
  divInt_nonneg_iff_of_pos_right (show 0 < (b : ℤ) by simpa using Nat.pos_of_ne_zero hb)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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