one_lt_mul_iff — Mathlib

English

Let α be a commutative monoid with a canonically ordered multiplication. Then 1 < a b holds exactly when 1 < a or 1 < b.

Русский

Пусть α — коммутативный моноид с канонически упорядоченным умножением. Тогда 1 < a b эквивалентно 1 < a или 1 < b.

LaTeX

$$$1 < a b \iff 1 < a \lor 1 < b$$$

Lean4

@[to_additive (attr := simp) add_pos_iff]
theorem one_lt_mul_iff : 1 < a * b ↔ 1 < a ∨ 1 < b := by simp only [one_lt_iff_ne_one, Ne, mul_eq_one, not_and_or]

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