Documentation

Mathlib.Algebra.Group.Invertible.Basic

Theorems about invertible elements #

@[simp]
theorem val_unitOfInvertible {α : Type u} [Monoid α] (a : α) [Invertible a] :
@[simp]
theorem val_inv_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
    • u.invertible = { invOf := u⁻¹, invOf_mul_self := , mul_invOf_self := }
    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]
        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] :
        @[reducible, inline]
        abbrev 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, inline]
          abbrev 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_symm_apply {α : Type u} [Monoid α] {a : α} :
            ∀ (x : Invertible a) (b : α) (x_1 : Invertible (a * b)), (x.mulLeft b).symm x_1 = invertibleOfInvertibleMul a b
            @[simp]
            theorem Invertible.mulLeft_apply {α : Type u} [Monoid α] {a : α} :
            ∀ (x : Invertible a) (b : α) (x_1 : Invertible b), (x.mulLeft b) x_1 = invertibleMul a b
            def Invertible.mulLeft {α : Type u} [Monoid α] {a : α} :
            Invertible a(b : α) → Invertible b Invertible (a * b)

            invertibleOfInvertibleMul and invertibleMul as an equivalence.

            Equations
            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
              Instances For
                instance invertiblePow {α : Type u} [Monoid α] (m : α) [Invertible m] (n : ) :
                Equations
                theorem invOf_pow {α : Type u} [Monoid α] (m : α) [Invertible m] (n : ) [Invertible (m ^ n)] :
                (m ^ n) = m ^ n
                def invertibleOfPowEqOne {α : Type u} [Monoid α] (x : α) (n : ) (hx : x ^ n = 1) (hn : n 0) :

                If x ^ n = 1 then x has an inverse, x^(n - 1).

                Equations
                Instances For
                  def Invertible.map {R : Type u_1} {S : Type u_2} {F : Type u_3} [MulOneClass R] [MulOneClass S] [FunLike F R S] [MonoidHomClass F R S] (f : F) (r : R) [Invertible 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] [FunLike F R 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] [FunLike G S R] [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] [FunLike G S R] [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_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [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
                      @[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] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [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
                      def invertibleEquivOfLeftInverse {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [Monoid R] [Monoid S] [FunLike F R S] [MonoidHomClass F R S] [FunLike G S R] [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