mul_pos

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.mul_pos

English

If both factors are nonzero, then their product is positive.

Русский

Если оба множителя не равны нулю, то их произведение положительно.

LaTeX

$$(a \neq 0 \land b \neq 0) \Rightarrow 0 < a \cdot b$$

Lean4

theorem mul_pos (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a * b :=
  mul_pos_iff.2 ⟨pos_iff_ne_zero.2 ha, pos_iff_ne_zero.2 hb⟩

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

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

Разделы

Аффилиация

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