div_pos_iff_of_pos_left

Mathlib.Algebra.Order.Field.Basic

URI: https://scilib.ai/kg/mathlib#div_pos_iff_of_pos_left

English

If 0 < a, then a/b > 0 if and only if 0 < b.

Русский

Если 0 < a, то a/b > 0 тогда и только тогда, когда 0 < b.

LaTeX

$$$0 < a \\Rightarrow (0 < a/b \\iff 0 < b)$$$

Lean4

@[simp]
theorem div_pos_iff_of_pos_left (ha : 0 < a) : 0 < a / b ↔ 0 < b := by
  simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]

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

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

Разделы

Аффилиация

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