mathlib3 documentation

algebra.order.invertible

Lemmas about inv_of in ordered (semi)rings. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[simp]
theorem inv_of_pos {α : Type u_1} [linear_ordered_semiring α] {a : α} [invertible a] :
0 < ⅟ a ↔ 0 < a
source
@[simp]
theorem inv_of_nonpos {α : Type u_1} [linear_ordered_semiring α] {a : α} [invertible a] :
⅟ a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem inv_of_nonneg {α : Type u_1} [linear_ordered_semiring α] {a : α} [invertible a] :
0 ≤ ⅟ a ↔ 0 ≤ a
source
@[simp]
theorem inv_of_lt_zero {α : Type u_1} [linear_ordered_semiring α] {a : α} [invertible a] :
⅟ a < 0 ↔ a < 0
source
@[simp]
theorem inv_of_le_one {α : Type u_1} [linear_ordered_semiring α] {a : α} [invertible a] (h : 1 ≤ a) :
⅟ a ≤ 1