Lemmas about invOf
in ordered (semi)rings. #
@[simp]
@[simp]
theorem
invOf_nonpos
{α : Type u_1}
[inst : LinearOrderedSemiring α]
{a : α}
[inst : Invertible a]
:
@[simp]
theorem
invOf_nonneg
{α : Type u_1}
[inst : LinearOrderedSemiring α]
{a : α}
[inst : Invertible a]
:
@[simp]
theorem
invOf_lt_zero
{α : Type u_1}
[inst : LinearOrderedSemiring α]
{a : α}
[inst : Invertible a]
:
@[simp]
theorem
invOf_le_one
{α : Type u_1}
[inst : LinearOrderedSemiring α]
{a : α}
[inst : Invertible a]
(h : 1 ≤ a)
:
theorem
pos_invOf_of_invertible_cast
{α : Type u_1}
[inst : LinearOrderedSemiring α]
[inst : Nontrivial α]
(n : ℕ)
[inst : Invertible ↑n]
: