Documentation

Mathlib.Algebra.Group.Invertible.Defs

Invertible elements #

This file defines a typeclass Invertible a for elements a with a two-sided multiplicative inverse.

The intent of the typeclass is to provide a way to write e.g. ⅟2 in a ring like ℤ[1/2] where some inverses exist but there is no general ⁻¹ operator; or to specify that a field has characteristic ≠ 2. It is the Type-valued analogue to the Prop-valued IsUnit.

For constructions of the invertible element given a characteristic, see Algebra/CharP/Invertible and other lemmas in that file.

Notation #

Implementation notes #

The Invertible class lives in Type, not Prop, to make computation easier. If multiplication is associative, Invertible is a subsingleton anyway.

The simp normal form tries to normalize ⅟a to a ⁻¹. Otherwise, it pushes inside the expression as much as possible.

Since Invertible a is not a Prop (but it is a Subsingleton), we have to be careful about coherence issues: we should avoid having multiple non-defeq instances for Invertible a in the same context. This file plays it safe and uses def rather than instance for most definitions, users can choose which instances to use at the point of use.

For example, here's how you can use an Invertible 1 instance:

variable {α : Type*} [Monoid α]

def something_that_needs_inverses (x : α) [Invertible x] := sorry

section
attribute [local instance] invertibleOne
def something_one := something_that_needs_inverses 1
end

Typeclass search vs. unification for simp lemmas #

Note that since typeclass search searches the local context first, an instance argument like [Invertible a] might sometimes be filled by a different term than the one we'd find by unification (i.e., the one that's used as an implicit argument to ).

This can cause issues with simp. Therefore, some lemmas are duplicated, with the @[simp] versions using unification and the user-facing ones using typeclass search.

Since unification can make backwards rewriting (e.g. rw [← mylemma]) impractical, we still want the instance-argument versions; therefore the user-facing versions retain the instance arguments and the original lemma name, whereas the @[simp]/unification ones acquire a ' at the end of their name.

We modify this file according to the above pattern only as needed; therefore, most @[simp] lemmas here are not part of such a duplicate pair. This is not (yet) intended as a permanent solution.

See Zulip: [https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Invertible.201.20simps/near/320558233]

Tags #

invertible, inverse element, invOf, a half, one half, a third, one third, ½, ⅓

class Invertible {α : Type u} [Mul α] [One α] (a : α) :

Invertible a gives a two-sided multiplicative inverse of a.

  • invOf : α

    The inverse of an Invertible element

  • invOf_mul_self : a * a = 1

    invOf a is a left inverse of a

  • mul_invOf_self : a * a = 1

    invOf a is a right inverse of a

Instances
    theorem Invertible.invOf_mul_self {α : Type u} :
    ∀ {inst : Mul α} {inst_1 : One α} {a : α} [self : Invertible a], a * a = 1

    invOf a is a left inverse of a

    theorem Invertible.mul_invOf_self {α : Type u} :
    ∀ {inst : Mul α} {inst_1 : One α} {a : α} [self : Invertible a], a * a = 1

    invOf a is a right inverse of a

    The inverse of an Invertible element

    Equations
    Instances For
      @[simp]
      theorem invOf_mul_self' {α : Type u} [Mul α] [One α] (a : α) :
      ∀ {x : Invertible a}, a * a = 1
      theorem invOf_mul_self {α : Type u} [Mul α] [One α] (a : α) [Invertible a] :
      a * a = 1
      @[simp]
      theorem mul_invOf_self' {α : Type u} [Mul α] [One α] (a : α) :
      ∀ {x : Invertible a}, a * a = 1
      theorem mul_invOf_self {α : Type u} [Mul α] [One α] (a : α) [Invertible a] :
      a * a = 1
      @[simp]
      theorem invOf_mul_cancel_left' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible a}, a * (a * b) = b
      theorem invOf_mul_cancel_left {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] :
      a * (a * b) = b
      @[deprecated invOf_mul_cancel_left']
      theorem invOf_mul_self_assoc' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible a}, a * (a * b) = b

      Alias of invOf_mul_cancel_left'.

      @[deprecated invOf_mul_cancel_left]
      theorem invOf_mul_self_assoc {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] :
      a * (a * b) = b

      Alias of invOf_mul_cancel_left.

      @[simp]
      theorem mul_invOf_cancel_left' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible a}, a * (a * b) = b
      theorem mul_invOf_cancel_left {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] :
      a * (a * b) = b
      @[deprecated mul_invOf_cancel_left']
      theorem mul_invOf_self_assoc' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible a}, a * (a * b) = b

      Alias of mul_invOf_cancel_left'.

      @[deprecated mul_invOf_cancel_left]
      theorem mul_invOf_self_assoc {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] :
      a * (a * b) = b

      Alias of mul_invOf_cancel_left.

      @[simp]
      theorem invOf_mul_cancel_right' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible b}, a * b * b = a
      theorem invOf_mul_cancel_right {α : Type u} [Monoid α] (a : α) (b : α) [Invertible b] :
      a * b * b = a
      @[deprecated invOf_mul_cancel_right']
      theorem mul_invOf_mul_self_cancel' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible b}, a * b * b = a

      Alias of invOf_mul_cancel_right'.

      @[deprecated invOf_mul_cancel_right]
      theorem mul_invOf_mul_self_cancel {α : Type u} [Monoid α] (a : α) (b : α) [Invertible b] :
      a * b * b = a

      Alias of invOf_mul_cancel_right.

      @[simp]
      theorem mul_invOf_cancel_right' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible b}, a * b * b = a
      theorem mul_invOf_cancel_right {α : Type u} [Monoid α] (a : α) (b : α) [Invertible b] :
      a * b * b = a
      @[deprecated mul_invOf_cancel_right']
      theorem mul_mul_invOf_self_cancel' {α : Type u} [Monoid α] (a : α) (b : α) :
      ∀ {x : Invertible b}, a * b * b = a

      Alias of mul_invOf_cancel_right'.

      @[deprecated mul_invOf_cancel_right]
      theorem mul_mul_invOf_self_cancel {α : Type u} [Monoid α] (a : α) (b : α) [Invertible b] :
      a * b * b = a

      Alias of mul_invOf_cancel_right.

      theorem invOf_eq_right_inv {α : Type u} [Monoid α] {a : α} {b : α} [Invertible a] (hac : a * b = 1) :
      a = b
      theorem invOf_eq_left_inv {α : Type u} [Monoid α] {a : α} {b : α} [Invertible a] (hac : b * a = 1) :
      a = b
      theorem invertible_unique {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] [Invertible b] (h : a = b) :
      instance Invertible.subsingleton {α : Type u} [Monoid α] (a : α) :
      Equations
      • =
      theorem Invertible.congr {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] [Invertible b] (h : a = b) :

      If a is invertible and a = b, then ⅟a = ⅟b.

      def Invertible.copy' {α : Type u} [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (si : α) (hs : s = r) (hsi : si = r) :

      If r is invertible and s = r and si = ⅟r, then s is invertible with ⅟s = si.

      Equations
      • hr.copy' s si hs hsi = { invOf := si, invOf_mul_self := , mul_invOf_self := }
      Instances For
        @[reducible, inline]
        abbrev Invertible.copy {α : Type u} [MulOneClass α] {r : α} (hr : Invertible r) (s : α) (hs : s = r) :

        If r is invertible and s = r, then s is invertible.

        Equations
        • hr.copy s hs = hr.copy' s (r) hs
        Instances For
          def invertibleOfGroup {α : Type u} [Group α] (a : α) :

          Each element of a group is invertible.

          Equations
          Instances For
            @[simp]
            theorem invOf_eq_group_inv {α : Type u} [Group α] (a : α) [Invertible a] :
            def invertibleOne {α : Type u} [Monoid α] :

            1 is the inverse of itself

            Equations
            • invertibleOne = { invOf := 1, invOf_mul_self := , mul_invOf_self := }
            Instances For
              @[simp]
              theorem invOf_one' {α : Type u} [Monoid α] :
              ∀ {x : Invertible 1}, 1 = 1
              theorem invOf_one {α : Type u} [Monoid α] [Invertible 1] :
              1 = 1
              instance invertibleInvOf {α : Type u} [One α] [Mul α] {a : α} [Invertible a] :

              a is the inverse of ⅟a.

              Equations
              • invertibleInvOf = { invOf := a, invOf_mul_self := , mul_invOf_self := }
              @[simp]
              theorem invOf_invOf {α : Type u} [Monoid α] (a : α) [Invertible a] [Invertible a] :
              @[simp]
              theorem invOf_inj {α : Type u} [Monoid α] {a : α} {b : α} [Invertible a] [Invertible b] :
              a = b a = b
              def invertibleMul {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] [Invertible b] :

              ⅟b * ⅟a is the inverse of a * b

              Equations
              Instances For
                @[simp]
                theorem invOf_mul {α : Type u} [Monoid α] (a : α) (b : α) [Invertible a] [Invertible b] [Invertible (a * b)] :
                (a * b) = b * a
                @[reducible, inline]
                abbrev Invertible.mul {α : Type u} [Monoid α] {a : α} {b : α} :
                Invertible aInvertible bInvertible (a * b)

                A copy of invertibleMul for dot notation.

                Equations
                Instances For
                  theorem mul_right_inj_of_invertible {α : Type u} [Monoid α] {a : α} {b : α} (c : α) [Invertible c] :
                  a * c = b * c a = b
                  theorem mul_left_inj_of_invertible {α : Type u} [Monoid α] {a : α} {b : α} (c : α) [Invertible c] :
                  c * a = c * b a = b
                  theorem invOf_mul_eq_iff_eq_mul_left {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] :
                  c * a = b a = c * b
                  theorem mul_left_eq_iff_eq_invOf_mul {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] :
                  c * a = b a = c * b
                  theorem mul_invOf_eq_iff_eq_mul_right {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] :
                  a * c = b a = b * c
                  theorem mul_right_eq_iff_eq_mul_invOf {α : Type u} [Monoid α] {a : α} {b : α} {c : α} [Invertible c] :
                  a * c = b a = b * c