invOf_pos — Mathlib

English

If n is a natural number and its image in a ordered ring is invertible, then its inverse is positive: 0 < (n : R)^{-1}.

Русский

Если n — натуральное число и образ n в упорядоченной полуреальности обратим, то его обратное положительно: 0 < (n : R)^{-1}.

LaTeX

$$$ 0 < \frac{1}{n} \quad\text{(in } R) \quad \text{for } n > 0 \text{ and } \text{Invertible}(n:R) $$$

Lean4

@[simp]
theorem invOf_pos [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⟩

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