mkRat_neg

Mathlib.Algebra.Order.Ring.Unbundled.Rat

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

English

If a < 0 and b ≠ 0, then mkRat a b < 0.

Русский

Если a < 0 и b ≠ 0, то a/b < 0.

LaTeX

$$$\\forall a \\in \\mathbb{Z},\\ a < 0 \\Rightarrow \\forall b \\in \\mathbb{N},\\ b \\neq 0 \\Rightarrow \\dfrac{a}{b} < 0$$$

Lean4

theorem mkRat_neg {a : ℤ} (ha : a < 0) {b : ℕ} (hb : b ≠ 0) : mkRat a b < 0 :=
  (mkRat_neg_iff a hb).mpr ha

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

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

Разделы

Аффилиация

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