invOf_nonneg — Mathlib

English

For invertible a in a linearly ordered ring, 0 ≤ ⅟a iff 0 ≤ a.

Русский

Для обратимого a в линейно упорядоченном кольце: 0 ≤ ⅟a ⇔ 0 ≤ a.

LaTeX

$$$ 0 \le ⅟a \iff 0 \le a $$$

Lean4

@[simp]
theorem invOf_nonneg [Invertible a] : 0 ≤ ⅟a ↔ 0 ≤ a :=
  haveI : 0 < a * ⅟a := by simp only [mul_invOf_self, zero_lt_one]
  ⟨fun h => (pos_of_mul_pos_left this h).le, fun h => (pos_of_mul_pos_right this h).le⟩

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