inv_neg — Mathlib

English

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

Русский

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

LaTeX

$$$↑u^{-1} < 0 \iff ↑u < 0$$$

Lean4

@[simp]
theorem inv_neg [ZeroLEOneClass R] [NeZero (1 : R)] [MulPosMono R] [PosMulMono R] {u : Rˣ} :
    ↑u⁻¹ < (0 : R) ↔ ↑u < (0 : R) :=
  have : ∀ {u : Rˣ}, ↑u < (0 : R) → ↑u⁻¹ < (0 : R) :=
    @fun u h => neg_of_mul_pos_right (u.mul_inv.symm ▸ zero_lt_one) h.le
  ⟨this, this⟩

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