Documentation

Mathlib.Algebra.Invertible.Basic

Theorems about invertible elements #

@[simp]
theorem val_inv_unitOfInvertible {α : Type u} [Monoid α] (a : α) [Invertible a] :
@[simp]
theorem val_unitOfInvertible {α : Type u} [Monoid α] (a : α) [Invertible a] :
def unitOfInvertible {α : Type u} [Monoid α] (a : α) [Invertible a] :
αˣ

An Invertible element is a unit.

Equations
Instances For
    theorem isUnit_of_invertible {α : Type u} [Monoid α] (a : α) [Invertible a] :
    def Units.invertible {α : Type u} [Monoid α] (u : αˣ) :

    Units are invertible in their associated monoid.

    Equations
    Instances For
      @[simp]
      theorem invOf_units {α : Type u} [Monoid α] (u : αˣ) [Invertible u] :
      u = u⁻¹
      theorem IsUnit.nonempty_invertible {α : Type u} [Monoid α] {a : α} (h : IsUnit a) :
      noncomputable def IsUnit.invertible {α : Type u} [Monoid α] {a : α} (h : IsUnit a) :

      Convert IsUnit to Invertible using Classical.choice.

      Prefer casesI h.nonempty_invertible over letI := h.invertible if you want to avoid choice.

      Equations
      Instances For
        @[simp]
        def invertibleNeg {α : Type u} [Mul α] [One α] [HasDistribNeg α] (a : α) [Invertible a] :

        -⅟a is the inverse of -a

        Equations
        Instances For
          @[simp]
          theorem invOf_neg {α : Type u} [Monoid α] [HasDistribNeg α] (a : α) [Invertible a] [Invertible (-a)] :
          (-a) = -a
          @[simp]
          theorem one_sub_invOf_two {α : Type u} [Ring α] [Invertible 2] :
          1 - 2 = 2
          @[simp]
          theorem Commute.invOf_right {α : Type u} [Monoid α] {a : α} {b : α} [Invertible b] (h : Commute a b) :
          theorem Commute.invOf_left {α : Type u} [Monoid α] {a : α} {b : α} [Invertible b] (h : Commute b a) :
          theorem commute_invOf {M : Type u_1} [One M] [Mul M] (m : M) [Invertible m] :
          theorem pos_of_invertible_cast {α : Type u} [Semiring α] [Nontrivial α] (n : ) [Invertible n] :
          0 < n
          @[reducible]
          def invertibleOfInvertibleMul {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] [Invertible (a * b)] :

          This is the Invertible version of Units.isUnit_units_mul

          Equations
          Instances For
            @[reducible]
            def invertibleOfMulInvertible {α : Type u} [Monoid α] (a : α) (b : α) [Invertible (a * b)] [Invertible b] :

            This is the Invertible version of Units.isUnit_mul_units

            Equations
            Instances For
              @[simp]
              theorem Invertible.mulLeft_apply {α : Type u} [Monoid α] {a : α} :
              ∀ (x : Invertible a) (b : α) (x_1 : Invertible b), ↑(Invertible.mulLeft x b) x_1 = invertibleMul a b
              @[simp]
              theorem Invertible.mulLeft_symm_apply {α : Type u} [Monoid α] {a : α} :
              ∀ (x : Invertible a) (b : α) (x_1 : Invertible (a * b)), (Invertible.mulLeft x b).symm x_1 = invertibleOfInvertibleMul a b
              def Invertible.mulLeft {α : Type u} [Monoid α] {a : α} :
              Invertible a(b : α) → Invertible b Invertible (a * b)

              invertibleOfInvertibleMul and invertibleMul as an equivalence.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Invertible.mulRight_symm_apply {α : Type u} [Monoid α] (a : α) {b : α} :
                ∀ (x : Invertible b) (x_1 : Invertible (a * b)), (Invertible.mulRight a x).symm x_1 = invertibleOfMulInvertible a b
                @[simp]
                theorem Invertible.mulRight_apply {α : Type u} [Monoid α] (a : α) {b : α} :
                ∀ (x : Invertible b) (x_1 : Invertible a), ↑(Invertible.mulRight a x) x_1 = invertibleMul a b
                def Invertible.mulRight {α : Type u} [Monoid α] (a : α) {b : α} :

                invertibleOfMulInvertible and invertibleMul as an equivalence.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Ring.inverse_invertible {α : Type u} [MonoidWithZero α] (x : α) [Invertible x] :

                  A variant of Ring.inverse_unit.

                  @[simp]
                  theorem div_mul_cancel_of_invertible {α : Type u} [GroupWithZero α] (a : α) (b : α) [Invertible b] :
                  a / b * b = a
                  @[simp]
                  theorem mul_div_cancel_of_invertible {α : Type u} [GroupWithZero α] (a : α) (b : α) [Invertible b] :
                  a * b / b = a
                  @[simp]
                  theorem div_self_of_invertible {α : Type u} [GroupWithZero α] (a : α) [Invertible a] :
                  a / a = 1
                  def invertibleDiv {α : Type u} [GroupWithZero α] (a : α) (b : α) [Invertible a] [Invertible b] :

                  b / a is the inverse of a / b

                  Equations
                  • invertibleDiv a b = { invOf := b / a, invOf_mul_self := (_ : b / a * (a / b) = 1), mul_invOf_self := (_ : a / b * (b / a) = 1) }
                  Instances For
                    theorem invOf_div {α : Type u} [GroupWithZero α] (a : α) (b : α) [Invertible a] [Invertible b] [Invertible (a / b)] :
                    (a / b) = b / a
                    def Invertible.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [MulOneClass R] [MulOneClass S] [MonoidHomClass F R S] (f : F) (r : R) [Invertible r] :
                    Invertible (f r)

                    Monoid homs preserve invertibility.

                    Equations
                    Instances For
                      theorem map_invOf {R : Type u_1} {S : Type u_2} {F : Type u_3} [MulOneClass R] [Monoid S] [MonoidHomClass F R S] (f : F) (r : R) [Invertible r] [ifr : Invertible (f r)] :
                      f r = (f r)

                      Note that the Invertible (f r) argument can be satisfied by using letI := Invertible.map f r before applying this lemma.

                      theorem Invertible.ofLeftInverse_invOf {R : Type u_1} {S : Type u_2} {G : Type u_3} [MulOneClass R] [MulOneClass S] [MonoidHomClass G S R] (f : RS) (g : G) (r : R) (h : Function.LeftInverse (g) f) [Invertible (f r)] :
                      r = (g (f r))
                      def Invertible.ofLeftInverse {R : Type u_1} {S : Type u_2} {G : Type u_3} [MulOneClass R] [MulOneClass S] [MonoidHomClass G S R] (f : RS) (g : G) (r : R) (h : Function.LeftInverse (g) f) [Invertible (f r)] :

                      If a function f : R → S has a left-inverse that is a monoid hom, then r : R is invertible if f r is.

                      The inverse is computed as g (⅟(f r))

                      Equations
                      Instances For
                        @[simp]
                        theorem invertibleEquivOfLeftInverse_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [Monoid R] [Monoid S] [MonoidHomClass F R S] [MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse g f) :
                        ∀ (x : Invertible r), (invertibleEquivOfLeftInverse f g r h).symm x = Invertible.map f r
                        @[simp]
                        theorem invertibleEquivOfLeftInverse_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [Monoid R] [Monoid S] [MonoidHomClass F R S] [MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse g f) :
                        ∀ (x : Invertible (f r)), ↑(invertibleEquivOfLeftInverse f g r h) x = Invertible.ofLeftInverse (f) g r h
                        def invertibleEquivOfLeftInverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [Monoid R] [Monoid S] [MonoidHomClass F R S] [MonoidHomClass G S R] (f : F) (g : G) (r : R) (h : Function.LeftInverse g f) :

                        Invertibility on either side of a monoid hom with a left-inverse is equivalent.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For