Documentation

Mathlib.Algebra.Order.Invertible

Lemmas about invOf in ordered (semi)rings. #

@[simp]
theorem invOf_pos {α : Type u_1} [inst : LinearOrderedSemiring α] {a : α} [inst : Invertible a] :
0 < a 0 < a
@[simp]
theorem invOf_nonpos {α : Type u_1} [inst : LinearOrderedSemiring α] {a : α} [inst : Invertible a] :
a 0 a 0
@[simp]
theorem invOf_nonneg {α : Type u_1} [inst : LinearOrderedSemiring α] {a : α} [inst : Invertible a] :
0 a 0 a
@[simp]
theorem invOf_lt_zero {α : Type u_1} [inst : LinearOrderedSemiring α] {a : α} [inst : Invertible a] :
a < 0 a < 0
@[simp]
theorem invOf_le_one {α : Type u_1} [inst : LinearOrderedSemiring α] {a : α} [inst : Invertible a] (h : 1 a) :
a 1
theorem pos_invOf_of_invertible_cast {α : Type u_1} [inst : LinearOrderedSemiring α] [inst : Nontrivial α] (n : ) [inst : Invertible n] :
0 < n