inv_pos — Mathlib

English

For units u in a semiring with ZeroLEOneClass, NeZero 1 and PosMulStrictMono, 0 < ↑u⁻¹ ↔ 0 < ↑u.

Русский

Для единиц u в полукольце с нулём-единицей, не ноль 1 и PosMulStrictMono, 0 < ↑u⁻¹ ↔ 0 < ↑u.

LaTeX

$$$(0 : R) < ↑u^{-1} \iff (0 : R) < ↑u$$$

Lean4

@[simp]
theorem inv_pos [ZeroLEOneClass R] [NeZero (1 : R)] [PosMulStrictMono R] {u : Rˣ} : (0 : R) < ↑u⁻¹ ↔ (0 : R) < u :=
  have : ∀ {u : Rˣ}, (0 : R) < u → (0 : R) < ↑u⁻¹ :=
    @fun u h => (mul_pos_iff_of_pos_left h).mp <| u.mul_inv.symm ▸ zero_lt_one
  ⟨this, this⟩

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