mathlib documentation

algebra.order.invertible

Lemmas about inv_of in ordered (semi)rings. #

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