Documentation

Mathlib.Algebra.Order.Invertible

Lemmas about invOf in ordered (semi)rings. #

source
@[simp]
theorem invOf_pos {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] :
0 < ⅟a ↔ 0 < a
source
@[simp]
theorem invOf_nonpos {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] :
⅟a ≤ 0 ↔ a ≤ 0
source
@[simp]
theorem invOf_nonneg {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] :
0 ≤ ⅟a ↔ 0 ≤ a
source
@[simp]
theorem invOf_lt_zero {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] :
⅟a < 0 ↔ a < 0
source
@[simp]
theorem invOf_le_one {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] (h : 1 ≤ a) :
⅟a ≤ 1
source
@[simp]
theorem invOf_lt_one {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} [Invertible a] (h : 1 < a) :
⅟a < 1
source
theorem pos_invOf_of_invertible_cast {R : Type u_1} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] (n : ℕ) [Invertible ↑n] :
0 < ⅟↑n