mul_pos

Mathlib.Algebra.Order.Ring.Canonical

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

← MathLib Explorer

English

For odd n, a^n < b^n iff a < b.

Русский

Для нечетного n, a^n < b^n эквивалентно a < b.

LaTeX

$$$a^n < b^n \iff a < b$$$

Lean4

@[simp]
protected theorem mul_pos [NoZeroDivisors R] {a b : R} : 0 < a * b ↔ 0 < a ∧ 0 < b := by
  simp only [pos_iff_ne_zero, ne_eq, mul_eq_zero, not_or]

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

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

Разделы

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

Аффилиация

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