Mathlib.Algebra.Order.Invertible

invOf_pos theorem

[Invertible a] : 0 < ⅟ a ↔ 0 < a

Full source

@[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⟩

Positivity of Inverse in Ordered Rings: $0 < ⅟a \leftrightarrow 0 < a$

Informal description

For any invertible element $a$ in a linearly ordered ring, the inverse of $a$ is positive if and only if $a$ itself is positive, i.e., $0 < ⅟a \leftrightarrow 0 < a$.

invOf_nonpos theorem

[Invertible a] : ⅟ a ≤ 0 ↔ a ≤ 0

Full source

@[simp]
theorem invOf_nonpos [Invertible a] : ⅟ a⅟ a ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, invOf_pos]

Inverse Nonpositivity Condition in Ordered Rings

Informal description

For any invertible element $a$ in a linearly ordered ring, the inverse of $a$ is nonpositive if and only if $a$ itself is nonpositive, i.e., $⅟a \leq 0 \leftrightarrow a \leq 0$.

invOf_nonneg theorem

[Invertible a] : 0 ≤ ⅟ a ↔ 0 ≤ a

Full source

@[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⟩

Inverse Nonnegativity Condition in Ordered Rings

Informal description

For any invertible element $a$ in a linearly ordered ring, the inverse of $a$ is nonnegative if and only if $a$ itself is nonnegative, i.e., $0 \leq ⅟a \leftrightarrow 0 \leq a$.

invOf_lt_zero theorem

[Invertible a] : ⅟ a < 0 ↔ a < 0

Full source

@[simp]
theorem invOf_lt_zero [Invertible a] : ⅟ a⅟ a < 0 ↔ a < 0 := by simp only [← not_le, invOf_nonneg]

Inverse is Negative if and only if Element is Negative

Informal description

For an invertible element $a$ in a linearly ordered ring, the inverse $\text{⅟} a$ is negative if and only if $a$ is negative, i.e., $\text{⅟} a < 0 \leftrightarrow a < 0$.

invOf_le_one theorem

[Invertible a] (h : 1 ≤ a) : ⅟ a ≤ 1

Full source

@[simp]
theorem invOf_le_one [Invertible a] (h : 1 ≤ a) : ⅟ a ≤ 1 :=
  mul_invOf_self a ▸ le_mul_of_one_le_left (invOf_nonneg.2 <| zero_le_one.trans h) h

Inverse of Greater-Than-One Element is Less-Than-Or-Equal-To-One: $1 \leq a \implies ⅟ a \leq 1$

Informal description

For any invertible element $a$ in a linearly ordered ring, if $1 \leq a$, then the inverse of $a$ satisfies $⅟ a \leq 1$.

pos_invOf_of_invertible_cast theorem

[Nontrivial R] (n : ℕ) [Invertible (n : R)] : 0 < ⅟ (n : R)

Full source

theorem pos_invOf_of_invertible_cast [Nontrivial R] (n : ℕ)
    [Invertible (n : R)] : 0 < ⅟(n : R) :=
  invOf_pos.2 <| Nat.cast_pos.2 <| pos_of_invertible_cast (R := R) n

Positivity of the Inverse of a Natural Number in an Ordered Semiring

Informal description

For any nontrivial ordered semiring $R$ and any natural number $n$ such that the cast of $n$ into $R$ is invertible, the inverse of $n$ in $R$ is positive, i.e., $0 < ⅟(n : R)$.