Invertible.lean

/-
Copyright (c) 2021 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
module

public import Mathlib.Algebra.Order.Ring.Defs
public import Mathlib.Algebra.Ring.Invertible
public import Mathlib.Data.Nat.Cast.Order.Ring

/-!
# Lemmas about `invOf` in ordered (semi)rings.
-/

public section

variable {R : Type*} [Semiring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R}

@[simp]
theorem invOf_pos [Invertible a] : 0 < ⅟a ↔ 0 < a :=
  haveI : 0 < a * ⅟a := by simp only [mul_invOf_self, zero_lt_one]
  ⟨fun h => pos_of_mul_pos_left this h.le, fun h => pos_of_mul_pos_right this h.le⟩

@[simp]
theorem invOf_nonpos [Invertible a] : ⅟a ≤ 0 ↔ a ≤ 0 := by simp only [← not_lt, invOf_pos]

@[simp]
theorem invOf_nonneg [Invertible a] : 0 ≤ ⅟a ↔ 0 ≤ a :=
  haveI : 0 < a * ⅟a := by simp only [mul_invOf_self, zero_lt_one]
  ⟨fun h => (pos_of_mul_pos_left this h).le, fun h => (pos_of_mul_pos_right this h).le⟩

@[simp]
theorem invOf_lt_zero [Invertible a] : ⅟a < 0 ↔ a < 0 := by simp only [← not_le, invOf_nonneg]

@[simp]
theorem invOf_le_one [Invertible a] (h : 1 ≤ a) : ⅟a ≤ 1 :=
  mul_invOf_self a ▸ le_mul_of_one_le_left (invOf_nonneg.2 <| zero_le_one.trans h) h

@[simp]
theorem invOf_lt_one [Invertible a] (h : 1 < a) : ⅟a < 1 :=
  mul_invOf_self a ▸ lt_mul_of_one_lt_left (invOf_pos.2 <| one_pos.trans h) h

theorem pos_invOf_of_invertible_cast (n : ℕ) [Invertible (n : R)] : 0 < ⅟(n : R) :=
  invOf_pos.2 <| Nat.cast_pos.2 <| pos_of_invertible_cast (R := R) n