pow_le_one_iff — Mathlib

English

For a linear-order monoid with left-monotone multiplication, for n ≠ 0, x^n ≤ 1 ⇔ x ≤ 1.

Русский

Для моноида с линейным порядком и монотонным умножением слева, при n ≠ 0 верно: x^n ≤ 1 ⇔ x ≤ 1.

LaTeX

$$$ n \neq 0 \Rightarrow (x^n \le 1 \iff x \le 1) $$$

Lean4

@[to_additive]
theorem pow_le_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n ≤ 1 ↔ x ≤ 1 :=
  one_le_pow_iff (M := Mᵒᵈ) hn

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