Documentation

Mathlib.Algebra.Group.Defs

Typeclasses for (semi)groups and monoids #

In this file we define typeclasses for algebraic structures with one binary operation. The classes are named (Add)?(Comm)?(Semigroup|Monoid|Group), where Add means that the class uses additive notation and Comm means that the class assumes that the binary operation is commutative.

The file does not contain any lemmas except for

For basic lemmas about these classes see Algebra.Group.Basic.

We also introduce notation classes SMul and VAdd for multiplicative and additive actions and register the following instances:

SMul is typically, but not exclusively, used for scalar multiplication-like operators. See the module Algebra.AddTorsor for a motivating example for the name VAdd (vector addition).

Notation #

class HVAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

The notation typeclass for heterogeneous additive actions. This enables the notation a +ᵥ b : γ where a : α, b : β.

  • hVAdd : αβγ

    a +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent.

Instances
    class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) :
    Type (max (max u v) w)

    The notation typeclass for heterogeneous scalar multiplication. This enables the notation a • b : γ where a : α, b : β.

    It is assumed to represent a left action in some sense. The notation a • b is augmented with a macro (below) to have it elaborate as a left action. Only the b argument participates in the elaboration algorithm: the algorithm uses the type of b when calculating the type of the surrounding arithmetic expression and it tries to insert coercions into b to get some b' such that a • b' has the same type as b'. See the module documentation near the macro for more details.

    • hSMul : αβγ

      a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

    Instances
      class VAdd (G : Type u) (P : Type v) :
      Type (max u v)

      Type class for the +ᵥ notation.

      • vadd : GPP

        a +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

      Instances
        class VSub (G : outParam (Type u_1)) (P : Type u_2) :
        Type (max u_1 u_2)

        Type class for the -ᵥ notation.

        • vsub : PPG

          a -ᵥ b computes the difference of a and b. The meaning of this notation is type-dependent, but it is intended to be used for additive torsors.

        Instances
          class SMul (M : Type u) (α : Type v) :
          Type (max u v)

          Typeclass for types with a scalar multiplication operation, denoted (\bu)

          • smul : Mαα

            a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

          Instances
            theorem SMul.ext {M : Type u} {α : Type v} {x : SMul M α} {y : SMul M α} (smul : SMul.smul = SMul.smul) :
            x = y
            theorem VAdd.ext {G : Type u} {P : Type v} {x : VAdd G P} {y : VAdd G P} (vadd : VAdd.vadd = VAdd.vadd) :
            x = y

            a +ᵥ b computes the sum of a and b. The meaning of this notation is type-dependent.

            Equations
            Instances For

              a -ᵥ b computes the difference of a and b. The meaning of this notation is type-dependent, but it is intended to be used for additive torsors.

              Equations
              Instances For

                a • b computes the product of a and b. The meaning of this notation is type-dependent, but it is intended to be used for left actions.

                Equations
                Instances For

                  We have a macro to make x • y notation participate in the expression tree elaborator, like other arithmetic expressions such as +, *, /, ^, =, inequalities, etc. The macro is using the leftact% elaborator introduced in this RFC.

                  As a concrete example of the effect of this macro, consider

                  variable [Ring R] [AddCommMonoid M] [Module R M] (r : R) (N : Submodule R M) (m : M) (n : N)
                  #check m + r • n
                  

                  Without the macro, the expression would elaborate as m + ↑(r • n : ↑N) : M. With the macro, the expression elaborates as m + r • (↑n : M) : M. To get the first interpretation, one can write m + (r • n :).

                  Here is a quick review of the expression tree elaborator:

                  1. It builds up an expression tree of all the immediately accessible operations that are marked with binop%, unop%, leftact%, rightact%, binrel%, etc.
                  2. It elaborates every leaf term of this tree (without an expected type, so as if it were temporarily wrapped in (... :)).
                  3. Using the types of each elaborated leaf, it computes a supremum type they can all be coerced to, if such a supremum exists.
                  4. It inserts coercions around leaf terms wherever needed.

                  The hypothesis is that individual expression trees tend to be calculations with respect to a single algebraic structure.

                  Note(kmill): If we were to remove HSMul and switch to using SMul directly, then the expression tree elaborator would not be able to insert coercions within the right operand; they would likely appear as ↑(x • y) rather than x • ↑y, unlike other arithmetic operations.

                  @[defaultInstance 1000]
                  instance instHSMul {α : Type u_1} {β : Type u_2} [SMul α β] :
                  HSMul α β β
                  Equations
                  • instHSMul = { hSMul := SMul.smul }
                  @[defaultInstance 1000]
                  instance instHVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] :
                  HVAdd α β β
                  Equations
                  • instHVAdd = { hVAdd := VAdd.vadd }
                  theorem SMul.smul_eq_hSMul {α : Type u_1} {β : Type u_2} [SMul α β] :
                  SMul.smul = HSMul.hSMul
                  theorem VAdd.vadd_eq_hVAdd {α : Type u_1} {β : Type u_2} [VAdd α β] :
                  VAdd.vadd = HVAdd.hVAdd
                  class Inv (α : Type u) :

                  Class of types that have an inversion operation.

                  • inv : αα

                    Invert an element of α.

                  Instances

                    Invert an element of α.

                    Equations
                    Instances For
                      @[simp]
                      theorem mul_dite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : α) (b : Pα) (c : ¬Pα) :
                      (a * if h : P then b h else c h) = if h : P then a * b h else a * c h
                      theorem add_dite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : α) (b : Pα) (c : ¬Pα) :
                      (a + if h : P then b h else c h) = if h : P then a + b h else a + c h
                      @[simp]
                      theorem mul_ite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : α) (b : α) (c : α) :
                      (a * if P then b else c) = if P then a * b else a * c
                      theorem add_ite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : α) (b : α) (c : α) :
                      (a + if P then b else c) = if P then a + b else a + c
                      @[simp]
                      theorem dite_mul {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : Pα) (b : ¬Pα) (c : α) :
                      (if h : P then a h else b h) * c = if h : P then a h * c else b h * c
                      theorem dite_add {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : Pα) (b : ¬Pα) (c : α) :
                      (if h : P then a h else b h) + c = if h : P then a h + c else b h + c
                      @[simp]
                      theorem ite_mul {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : α) (b : α) (c : α) :
                      (if P then a else b) * c = if P then a * c else b * c
                      theorem ite_add {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : α) (b : α) (c : α) :
                      (if P then a else b) + c = if P then a + c else b + c
                      theorem dite_mul_dite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : Pα) (b : ¬Pα) (c : Pα) (d : ¬Pα) :
                      ((if h : P then a h else b h) * if h : P then c h else d h) = if h : P then a h * c h else b h * d h
                      theorem dite_add_dite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : Pα) (b : ¬Pα) (c : Pα) (d : ¬Pα) :
                      ((if h : P then a h else b h) + if h : P then c h else d h) = if h : P then a h + c h else b h + d h
                      theorem ite_mul_ite {α : Type u_2} (P : Prop) [Decidable P] [Mul α] (a : α) (b : α) (c : α) (d : α) :
                      ((if P then a else b) * if P then c else d) = if P then a * c else b * d
                      theorem ite_add_ite {α : Type u_2} (P : Prop) [Decidable P] [Add α] (a : α) (b : α) (c : α) (d : α) :
                      ((if P then a else b) + if P then c else d) = if P then a + c else b + d
                      theorem div_dite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : α) (b : Pα) (c : ¬Pα) :
                      (a / if h : P then b h else c h) = if h : P then a / b h else a / c h
                      theorem sub_dite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : α) (b : Pα) (c : ¬Pα) :
                      (a - if h : P then b h else c h) = if h : P then a - b h else a - c h
                      theorem div_ite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : α) (b : α) (c : α) :
                      (a / if P then b else c) = if P then a / b else a / c
                      theorem sub_ite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : α) (b : α) (c : α) :
                      (a - if P then b else c) = if P then a - b else a - c
                      theorem dite_div {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : Pα) (b : ¬Pα) (c : α) :
                      (if h : P then a h else b h) / c = if h : P then a h / c else b h / c
                      theorem dite_sub {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : Pα) (b : ¬Pα) (c : α) :
                      (if h : P then a h else b h) - c = if h : P then a h - c else b h - c
                      theorem ite_div {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : α) (b : α) (c : α) :
                      (if P then a else b) / c = if P then a / c else b / c
                      theorem ite_sub {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : α) (b : α) (c : α) :
                      (if P then a else b) - c = if P then a - c else b - c
                      theorem dite_div_dite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : Pα) (b : ¬Pα) (c : Pα) (d : ¬Pα) :
                      ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h
                      theorem dite_sub_dite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : Pα) (b : ¬Pα) (c : Pα) (d : ¬Pα) :
                      ((if h : P then a h else b h) - if h : P then c h else d h) = if h : P then a h - c h else b h - d h
                      theorem ite_div_ite {α : Type u_2} (P : Prop) [Decidable P] [Div α] (a : α) (b : α) (c : α) (d : α) :
                      ((if P then a else b) / if P then c else d) = if P then a / c else b / d
                      theorem ite_sub_ite {α : Type u_2} (P : Prop) [Decidable P] [Sub α] (a : α) (b : α) (c : α) (d : α) :
                      ((if P then a else b) - if P then c else d) = if P then a - c else b - d
                      def leftMul {G : Type u_1} [Mul G] :
                      GGG

                      leftMul g denotes left multiplication by g

                      Equations
                      Instances For
                        def leftAdd {G : Type u_1} [Add G] :
                        GGG

                        leftAdd g denotes left addition by g

                        Equations
                        Instances For
                          def rightMul {G : Type u_1} [Mul G] :
                          GGG

                          rightMul g denotes right multiplication by g

                          Equations
                          Instances For
                            def rightAdd {G : Type u_1} [Add G] :
                            GGG

                            rightAdd g denotes right addition by g

                            Equations
                            Instances For
                              class IsLeftCancelMul (G : Type u) [Mul G] :

                              A mixin for left cancellative multiplication.

                              • mul_left_cancel : ∀ (a b c : G), a * b = a * cb = c

                                Multiplication is left cancellative.

                              Instances
                                theorem IsLeftCancelMul.mul_left_cancel {G : Type u} :
                                ∀ {inst : Mul G} [self : IsLeftCancelMul G] (a b c : G), a * b = a * cb = c

                                Multiplication is left cancellative.

                                class IsRightCancelMul (G : Type u) [Mul G] :

                                A mixin for right cancellative multiplication.

                                • mul_right_cancel : ∀ (a b c : G), a * b = c * ba = c

                                  Multiplication is right cancellative.

                                Instances
                                  theorem IsRightCancelMul.mul_right_cancel {G : Type u} :
                                  ∀ {inst : Mul G} [self : IsRightCancelMul G] (a b c : G), a * b = c * ba = c

                                  Multiplication is right cancellative.

                                  A mixin for cancellative multiplication.

                                    Instances
                                      class IsLeftCancelAdd (G : Type u) [Add G] :

                                      A mixin for left cancellative addition.

                                      • add_left_cancel : ∀ (a b c : G), a + b = a + cb = c

                                        Addition is left cancellative.

                                      Instances
                                        theorem IsLeftCancelAdd.add_left_cancel {G : Type u} :
                                        ∀ {inst : Add G} [self : IsLeftCancelAdd G] (a b c : G), a + b = a + cb = c

                                        Addition is left cancellative.

                                        class IsRightCancelAdd (G : Type u) [Add G] :

                                        A mixin for right cancellative addition.

                                        • add_right_cancel : ∀ (a b c : G), a + b = c + ba = c

                                          Addition is right cancellative.

                                        Instances
                                          theorem IsRightCancelAdd.add_right_cancel {G : Type u} :
                                          ∀ {inst : Add G} [self : IsRightCancelAdd G] (a b c : G), a + b = c + ba = c

                                          Addition is right cancellative.

                                          A mixin for cancellative addition.

                                            Instances
                                              theorem mul_left_cancel {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a : G} {b : G} {c : G} :
                                              a * b = a * cb = c
                                              theorem add_left_cancel {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a : G} {b : G} {c : G} :
                                              a + b = a + cb = c
                                              theorem mul_left_cancel_iff {G : Type u_1} [Mul G] [IsLeftCancelMul G] {a : G} {b : G} {c : G} :
                                              a * b = a * c b = c
                                              theorem add_left_cancel_iff {G : Type u_1} [Add G] [IsLeftCancelAdd G] {a : G} {b : G} {c : G} :
                                              a + b = a + c b = c
                                              theorem mul_right_cancel {G : Type u_1} [Mul G] [IsRightCancelMul G] {a : G} {b : G} {c : G} :
                                              a * b = c * ba = c
                                              theorem add_right_cancel {G : Type u_1} [Add G] [IsRightCancelAdd G] {a : G} {b : G} {c : G} :
                                              a + b = c + ba = c
                                              theorem mul_right_cancel_iff {G : Type u_1} [Mul G] [IsRightCancelMul G] {a : G} {b : G} {c : G} :
                                              b * a = c * a b = c
                                              theorem add_right_cancel_iff {G : Type u_1} [Add G] [IsRightCancelAdd G] {a : G} {b : G} {c : G} :
                                              b + a = c + a b = c
                                              class Semigroup (G : Type u) extends Mul :

                                              A semigroup is a type with an associative (*).

                                              • mul : GGG
                                              • mul_assoc : ∀ (a b c : G), a * b * c = a * (b * c)

                                                Multiplication is associative

                                              Instances
                                                theorem Semigroup.ext {G : Type u} {x : Semigroup G} {y : Semigroup G} (mul : Mul.mul = Mul.mul) :
                                                x = y
                                                theorem Semigroup.mul_assoc {G : Type u} [self : Semigroup G] (a : G) (b : G) (c : G) :
                                                a * b * c = a * (b * c)

                                                Multiplication is associative

                                                class AddSemigroup (G : Type u) extends Add :

                                                An additive semigroup is a type with an associative (+).

                                                • add : GGG
                                                • add_assoc : ∀ (a b c : G), a + b + c = a + (b + c)

                                                  Addition is associative

                                                Instances
                                                  theorem AddSemigroup.ext {G : Type u} {x : AddSemigroup G} {y : AddSemigroup G} (add : Add.add = Add.add) :
                                                  x = y
                                                  theorem AddSemigroup.add_assoc {G : Type u} [self : AddSemigroup G] (a : G) (b : G) (c : G) :
                                                  a + b + c = a + (b + c)

                                                  Addition is associative

                                                  theorem mul_assoc {G : Type u_1} [Semigroup G] (a : G) (b : G) (c : G) :
                                                  a * b * c = a * (b * c)
                                                  theorem add_assoc {G : Type u_1} [AddSemigroup G] (a : G) (b : G) (c : G) :
                                                  a + b + c = a + (b + c)
                                                  class AddCommMagma (G : Type u) extends Add :

                                                  A commutative additive magma is a type with an addition which commutes.

                                                  • add : GGG
                                                  • add_comm : ∀ (a b : G), a + b = b + a

                                                    Addition is commutative in an commutative additive magma.

                                                  Instances
                                                    theorem AddCommMagma.ext {G : Type u} {x : AddCommMagma G} {y : AddCommMagma G} (add : Add.add = Add.add) :
                                                    x = y
                                                    theorem AddCommMagma.add_comm {G : Type u} [self : AddCommMagma G] (a : G) (b : G) :
                                                    a + b = b + a

                                                    Addition is commutative in an commutative additive magma.

                                                    class CommMagma (G : Type u) extends Mul :

                                                    A commutative multiplicative magma is a type with a multiplication which commutes.

                                                    • mul : GGG
                                                    • mul_comm : ∀ (a b : G), a * b = b * a

                                                      Multiplication is commutative in a commutative multiplicative magma.

                                                    Instances
                                                      theorem CommMagma.ext {G : Type u} {x : CommMagma G} {y : CommMagma G} (mul : Mul.mul = Mul.mul) :
                                                      x = y
                                                      theorem CommMagma.mul_comm {G : Type u} [self : CommMagma G] (a : G) (b : G) :
                                                      a * b = b * a

                                                      Multiplication is commutative in a commutative multiplicative magma.

                                                      class CommSemigroup (G : Type u) extends Semigroup , CommMagma , Mul :

                                                      A commutative semigroup is a type with an associative commutative (*).

                                                        Instances
                                                          theorem CommSemigroup.ext {G : Type u} {x : CommSemigroup G} {y : CommSemigroup G} (mul : Mul.mul = Mul.mul) :
                                                          x = y
                                                          class AddCommSemigroup (G : Type u) extends AddSemigroup , AddCommMagma , Add :

                                                          A commutative additive semigroup is a type with an associative commutative (+).

                                                            Instances
                                                              theorem AddCommSemigroup.ext {G : Type u} {x : AddCommSemigroup G} {y : AddCommSemigroup G} (add : Add.add = Add.add) :
                                                              x = y
                                                              theorem mul_comm {G : Type u_1} [CommMagma G] (a : G) (b : G) :
                                                              a * b = b * a
                                                              theorem add_comm {G : Type u_1} [AddCommMagma G] (a : G) (b : G) :
                                                              a + b = b + a
                                                              class LeftCancelSemigroup (G : Type u) extends Semigroup , Mul :

                                                              A LeftCancelSemigroup is a semigroup such that a * b = a * c implies b = c.

                                                                Instances
                                                                  theorem LeftCancelSemigroup.ext {G : Type u} {x : LeftCancelSemigroup G} {y : LeftCancelSemigroup G} (mul : Mul.mul = Mul.mul) :
                                                                  x = y
                                                                  theorem LeftCancelSemigroup.mul_left_cancel {G : Type u} [self : LeftCancelSemigroup G] (a : G) (b : G) (c : G) :
                                                                  a * b = a * cb = c
                                                                  class AddLeftCancelSemigroup (G : Type u) extends AddSemigroup , Add :

                                                                  An AddLeftCancelSemigroup is an additive semigroup such that a + b = a + c implies b = c.

                                                                    Instances
                                                                      theorem AddLeftCancelSemigroup.ext {G : Type u} {x : AddLeftCancelSemigroup G} {y : AddLeftCancelSemigroup G} (add : Add.add = Add.add) :
                                                                      x = y
                                                                      theorem AddLeftCancelSemigroup.add_left_cancel {G : Type u} [self : AddLeftCancelSemigroup G] (a : G) (b : G) (c : G) :
                                                                      a + b = a + cb = c
                                                                      class RightCancelSemigroup (G : Type u) extends Semigroup , Mul :

                                                                      A RightCancelSemigroup is a semigroup such that a * b = c * b implies a = c.

                                                                        Instances
                                                                          theorem RightCancelSemigroup.ext {G : Type u} {x : RightCancelSemigroup G} {y : RightCancelSemigroup G} (mul : Mul.mul = Mul.mul) :
                                                                          x = y
                                                                          theorem RightCancelSemigroup.mul_right_cancel {G : Type u} [self : RightCancelSemigroup G] (a : G) (b : G) (c : G) :
                                                                          a * b = c * ba = c
                                                                          class AddRightCancelSemigroup (G : Type u) extends AddSemigroup , Add :

                                                                          An AddRightCancelSemigroup is an additive semigroup such that a + b = c + b implies a = c.

                                                                            Instances
                                                                              theorem AddRightCancelSemigroup.ext {G : Type u} {x : AddRightCancelSemigroup G} {y : AddRightCancelSemigroup G} (add : Add.add = Add.add) :
                                                                              x = y
                                                                              theorem AddRightCancelSemigroup.add_right_cancel {G : Type u} [self : AddRightCancelSemigroup G] (a : G) (b : G) (c : G) :
                                                                              a + b = c + ba = c
                                                                              class MulOneClass (M : Type u) extends One , Mul :

                                                                              Typeclass for expressing that a type M with multiplication and a one satisfies 1 * a = a and a * 1 = a for all a : M.

                                                                              • one : M
                                                                              • mul : MMM
                                                                              • one_mul : ∀ (a : M), 1 * a = a

                                                                                One is a left neutral element for multiplication

                                                                              • mul_one : ∀ (a : M), a * 1 = a

                                                                                One is a right neutral element for multiplication

                                                                              Instances
                                                                                theorem MulOneClass.one_mul {M : Type u} [self : MulOneClass M] (a : M) :
                                                                                1 * a = a

                                                                                One is a left neutral element for multiplication

                                                                                theorem MulOneClass.mul_one {M : Type u} [self : MulOneClass M] (a : M) :
                                                                                a * 1 = a

                                                                                One is a right neutral element for multiplication

                                                                                class AddZeroClass (M : Type u) extends Zero , Add :

                                                                                Typeclass for expressing that a type M with addition and a zero satisfies 0 + a = a and a + 0 = a for all a : M.

                                                                                • zero : M
                                                                                • add : MMM
                                                                                • zero_add : ∀ (a : M), 0 + a = a

                                                                                  Zero is a left neutral element for addition

                                                                                • add_zero : ∀ (a : M), a + 0 = a

                                                                                  Zero is a right neutral element for addition

                                                                                Instances
                                                                                  theorem AddZeroClass.zero_add {M : Type u} [self : AddZeroClass M] (a : M) :
                                                                                  0 + a = a

                                                                                  Zero is a left neutral element for addition

                                                                                  theorem AddZeroClass.add_zero {M : Type u} [self : AddZeroClass M] (a : M) :
                                                                                  a + 0 = a

                                                                                  Zero is a right neutral element for addition

                                                                                  theorem AddZeroClass.ext {M : Type u} ⦃m₁ : AddZeroClass M ⦃m₂ : AddZeroClass M :
                                                                                  Add.add = Add.addm₁ = m₂
                                                                                  theorem MulOneClass.ext {M : Type u} ⦃m₁ : MulOneClass M ⦃m₂ : MulOneClass M :
                                                                                  Mul.mul = Mul.mulm₁ = m₂
                                                                                  @[simp]
                                                                                  theorem one_mul {M : Type u} [MulOneClass M] (a : M) :
                                                                                  1 * a = a
                                                                                  @[simp]
                                                                                  theorem zero_add {M : Type u} [AddZeroClass M] (a : M) :
                                                                                  0 + a = a
                                                                                  @[simp]
                                                                                  theorem mul_one {M : Type u} [MulOneClass M] (a : M) :
                                                                                  a * 1 = a
                                                                                  @[simp]
                                                                                  theorem add_zero {M : Type u} [AddZeroClass M] (a : M) :
                                                                                  a + 0 = a
                                                                                  def npowRec {M : Type u} [One M] [Mul M] :
                                                                                  MM

                                                                                  The fundamental power operation in a monoid. npowRec n a = a*a*...*a n times. Use instead a ^ n, which has better definitional behavior.

                                                                                  Equations
                                                                                  Instances For
                                                                                    def nsmulRec {M : Type u} [Zero M] [Add M] :
                                                                                    MM

                                                                                    The fundamental scalar multiplication in an additive monoid. nsmulRec n a = a+a+...+a n times. Use instead n • a, which has better definitional behavior.

                                                                                    Equations
                                                                                    Instances For
                                                                                      theorem npowRec_add {M : Type u} [One M] [Semigroup M] (m : ) (n : ) (hn : n 0) (a : M) (ha : 1 * a = a) :
                                                                                      npowRec (m + n) a = npowRec m a * npowRec n a
                                                                                      theorem nsmulRec_add {M : Type u} [Zero M] [AddSemigroup M] (m : ) (n : ) (hn : n 0) (a : M) (ha : 0 + a = a) :
                                                                                      nsmulRec (m + n) a = nsmulRec m a + nsmulRec n a
                                                                                      theorem npowRec_succ {M : Type u} [One M] [Semigroup M] (n : ) (hn : n 0) (a : M) (ha : 1 * a = a) :
                                                                                      npowRec (n + 1) a = a * npowRec n a
                                                                                      theorem nsmulRec_succ {M : Type u} [Zero M] [AddSemigroup M] (n : ) (hn : n 0) (a : M) (ha : 0 + a = a) :
                                                                                      nsmulRec (n + 1) a = a + nsmulRec n a

                                                                                      Design note on AddMonoid and Monoid #

                                                                                      An AddMonoid has a natural -action, defined by n • a = a + ... + a, that we want to declare as an instance as it makes it possible to use the language of linear algebra. However, there are often other natural -actions. For instance, for any semiring R, the space of polynomials Polynomial R has a natural R-action defined by multiplication on the coefficients. This means that Polynomial ℕ would have two natural -actions, which are equal but not defeq. The same goes for linear maps, tensor products, and so on (and even for itself).

                                                                                      To solve this issue, we embed an -action in the definition of an AddMonoid (which is by default equal to the naive action a + ... + a, but can be adjusted when needed), and declare a SMul ℕ α instance using this action. See Note [forgetful inheritance] for more explanations on this pattern.

                                                                                      For example, when we define Polynomial R, then we declare the -action to be by multiplication on each coefficient (using the -action on R that comes from the fact that R is an AddMonoid). In this way, the two natural SMul ℕ (Polynomial ℕ) instances are defeq.

                                                                                      The tactic to_additive transfers definitions and results from multiplicative monoids to additive monoids. To work, it has to map fields to fields. This means that we should also add corresponding fields to the multiplicative structure Monoid, which could solve defeq problems for powers if needed. These problems do not come up in practice, so most of the time we will not need to adjust the npow field when defining multiplicative objects.

                                                                                      def nsmulBinRec {M : Type u_2} [Zero M] [Add M] (k : ) (m : M) :
                                                                                      M

                                                                                      Scalar multiplication by repeated self-addition, the additive version of exponentation by repeated squaring.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[irreducible]
                                                                                        def nsmulBinRec.go {M : Type u_2} [Add M] :
                                                                                        MMM

                                                                                        Auxiliary tail-recursive implementation for nsmulBinRec

                                                                                        Equations
                                                                                        Instances For
                                                                                          def npowBinRec {M : Type u_2} [One M] [Mul M] (k : ) (m : M) :
                                                                                          M

                                                                                          Exponentiation by repeated squaring.

                                                                                          Equations
                                                                                          Instances For
                                                                                            @[irreducible]
                                                                                            def npowBinRec.go {M : Type u_2} [Mul M] :
                                                                                            MMM

                                                                                            Auxiliary tail-recursive implementation for npowBinRec

                                                                                            Equations
                                                                                            Instances For
                                                                                              def npowRec' {M : Type u_2} [One M] [Mul M] :
                                                                                              MM

                                                                                              A variant of npowRec which is a semigroup homomorphisms from ℕ₊ to M.

                                                                                              Equations
                                                                                              Instances For
                                                                                                def nsmulRec' {M : Type u_2} [Zero M] [Add M] :
                                                                                                MM

                                                                                                A variant of nsmulRec which is a semigroup homomorphisms from ℕ₊ to M.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  theorem npowRec'_succ {M : Type u_2} [Semigroup M] [One M] (k : ) (m : M) :
                                                                                                  npowRec' (k + 2) m = npowRec' (k + 1) m * m
                                                                                                  theorem nsmulRec'_succ {M : Type u_2} [AddSemigroup M] [Zero M] (k : ) (m : M) :
                                                                                                  nsmulRec' (k + 2) m = nsmulRec' (k + 1) m + m
                                                                                                  theorem npowRec'_two_mul {M : Type u_2} [Semigroup M] [One M] (k : ) (m : M) :
                                                                                                  npowRec' (2 * k) m = npowRec' k (m * m)
                                                                                                  theorem nsmulRec'_two_add {M : Type u_2} [AddSemigroup M] [Zero M] (k : ) (m : M) :
                                                                                                  nsmulRec' (2 * k) m = nsmulRec' k (m + m)
                                                                                                  theorem npowRec'_mul_comm {M : Type u_2} [Semigroup M] [One M] (k : ) (m : M) :
                                                                                                  m * npowRec' (k + 1) m = npowRec' (k + 1) m * m
                                                                                                  theorem nsmulRec'_add_comm {M : Type u_2} [AddSemigroup M] [Zero M] (k : ) (m : M) :
                                                                                                  m + nsmulRec' (k + 1) m = nsmulRec' (k + 1) m + m
                                                                                                  theorem npowRec_eq {M : Type u_2} [Semigroup M] [One M] (k : ) (m : M) :
                                                                                                  npowRec (k + 1) m = 1 * npowRec' (k + 1) m
                                                                                                  theorem nsmulRec_eq {M : Type u_2} [AddSemigroup M] [Zero M] (k : ) (m : M) :
                                                                                                  nsmulRec (k + 1) m = 0 + nsmulRec' (k + 1) m
                                                                                                  theorem npowBinRec.go_spec {M : Type u_2} [Semigroup M] [One M] (k : ) (m : M) (n : M) :
                                                                                                  npowBinRec.go (k + 1) m n = m * npowRec' (k + 1) n
                                                                                                  theorem nsmulBinRec.go_spec {M : Type u_2} [AddSemigroup M] [Zero M] (k : ) (m : M) (n : M) :
                                                                                                  nsmulBinRec.go (k + 1) m n = m + nsmulRec' (k + 1) n
                                                                                                  @[reducible, inline]
                                                                                                  abbrev npowRecAuto {M : Type u_2} [Semigroup M] [One M] (k : ) (m : M) :
                                                                                                  M

                                                                                                  An abbreviation for npowRec with an additional typeclass assumption on associativity so that we can use @[csimp] to replace it with an implementation by repeated squaring in compiled code.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[reducible, inline]
                                                                                                    abbrev nsmulRecAuto {M : Type u_2} [AddSemigroup M] [Zero M] (k : ) (m : M) :
                                                                                                    M

                                                                                                    An abbreviation for nsmulRec with an additional typeclass assumptions on associativity so that we can use @[csimp] to replace it with an implementation by repeated doubling in compiled code as an automatic parameter.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[reducible, inline]
                                                                                                      abbrev npowBinRecAuto {M : Type u_2} [Semigroup M] [One M] (k : ) (m : M) :
                                                                                                      M

                                                                                                      An abbreviation for npowBinRec with an additional typeclass assumption on associativity so that we can use it in @[csimp] for more performant code generation.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[reducible, inline]
                                                                                                        abbrev nsmulBinRecAuto {M : Type u_2} [AddSemigroup M] [Zero M] (k : ) (m : M) :
                                                                                                        M

                                                                                                        An abbreviation for nsmulBinRec with an additional typeclass assumption on associativity so that we can use it in @[csimp] for more performant code generation as an automatic parameter.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          class AddMonoid (M : Type u) extends AddSemigroup , AddZeroClass , Zero , Add :

                                                                                                          An AddMonoid is an AddSemigroup with an element 0 such that 0 + a = a + 0 = a.

                                                                                                          • add : MMM
                                                                                                          • add_assoc : ∀ (a b c : M), a + b + c = a + (b + c)
                                                                                                          • zero : M
                                                                                                          • zero_add : ∀ (a : M), 0 + a = a

                                                                                                            Zero is a left neutral element for addition

                                                                                                          • add_zero : ∀ (a : M), a + 0 = a

                                                                                                            Zero is a right neutral element for addition

                                                                                                          • nsmul : MM

                                                                                                            Multiplication by a natural number. Set this to nsmulRec unless Module diamonds are possible.

                                                                                                          • nsmul_zero : ∀ (x : M), AddMonoid.nsmul 0 x = 0

                                                                                                            Multiplication by (0 : ℕ) gives 0.

                                                                                                          • nsmul_succ : ∀ (n : ) (x : M), AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x

                                                                                                            Multiplication by (n + 1 : ℕ) behaves as expected.

                                                                                                          Instances
                                                                                                            theorem AddMonoid.nsmul_zero {M : Type u} [self : AddMonoid M] (x : M) :

                                                                                                            Multiplication by (0 : ℕ) gives 0.

                                                                                                            theorem AddMonoid.nsmul_succ {M : Type u} [self : AddMonoid M] (n : ) (x : M) :

                                                                                                            Multiplication by (n + 1 : ℕ) behaves as expected.

                                                                                                            class Monoid (M : Type u) extends Semigroup , MulOneClass , One , Mul :

                                                                                                            A Monoid is a Semigroup with an element 1 such that 1 * a = a * 1 = a.

                                                                                                            • mul : MMM
                                                                                                            • mul_assoc : ∀ (a b c : M), a * b * c = a * (b * c)
                                                                                                            • one : M
                                                                                                            • one_mul : ∀ (a : M), 1 * a = a

                                                                                                              One is a left neutral element for multiplication

                                                                                                            • mul_one : ∀ (a : M), a * 1 = a

                                                                                                              One is a right neutral element for multiplication

                                                                                                            • npow : MM

                                                                                                              Raising to the power of a natural number.

                                                                                                            • npow_zero : ∀ (x : M), Monoid.npow 0 x = 1

                                                                                                              Raising to the power (0 : ℕ) gives 1.

                                                                                                            • npow_succ : ∀ (n : ) (x : M), Monoid.npow (n + 1) x = Monoid.npow n x * x

                                                                                                              Raising to the power (n + 1 : ℕ) behaves as expected.

                                                                                                            Instances
                                                                                                              theorem Monoid.npow_zero {M : Type u} [self : Monoid M] (x : M) :

                                                                                                              Raising to the power (0 : ℕ) gives 1.

                                                                                                              theorem Monoid.npow_succ {M : Type u} [self : Monoid M] (n : ) (x : M) :
                                                                                                              Monoid.npow (n + 1) x = Monoid.npow n x * x

                                                                                                              Raising to the power (n + 1 : ℕ) behaves as expected.

                                                                                                              @[defaultInstance 10000]
                                                                                                              instance Monoid.toNatPow {M : Type u_2} [Monoid M] :
                                                                                                              Equations
                                                                                                              instance AddMonoid.toNatSMul {M : Type u_2} [AddMonoid M] :
                                                                                                              Equations
                                                                                                              • AddMonoid.toNatSMul = { smul := AddMonoid.nsmul }
                                                                                                              @[simp]
                                                                                                              theorem npow_eq_pow {M : Type u_2} [Monoid M] (n : ) (x : M) :
                                                                                                              Monoid.npow n x = x ^ n
                                                                                                              @[simp]
                                                                                                              theorem nsmul_eq_smul {M : Type u_2} [AddMonoid M] (n : ) (x : M) :
                                                                                                              theorem left_inv_eq_right_inv {M : Type u_2} [Monoid M] {a : M} {b : M} {c : M} (hba : b * a = 1) (hac : a * c = 1) :
                                                                                                              b = c
                                                                                                              theorem left_neg_eq_right_neg {M : Type u_2} [AddMonoid M] {a : M} {b : M} {c : M} (hba : b + a = 0) (hac : a + c = 0) :
                                                                                                              b = c
                                                                                                              @[simp]
                                                                                                              theorem pow_zero {M : Type u_2} [Monoid M] (a : M) :
                                                                                                              a ^ 0 = 1
                                                                                                              theorem zero_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
                                                                                                              0 a = 0
                                                                                                              theorem pow_succ {M : Type u_2} [Monoid M] (a : M) (n : ) :
                                                                                                              a ^ (n + 1) = a ^ n * a
                                                                                                              theorem succ_nsmul {M : Type u_2} [AddMonoid M] (a : M) (n : ) :
                                                                                                              (n + 1) a = n a + a
                                                                                                              @[simp]
                                                                                                              theorem pow_one {M : Type u_2} [Monoid M] (a : M) :
                                                                                                              a ^ 1 = a
                                                                                                              @[simp]
                                                                                                              theorem one_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
                                                                                                              1 a = a
                                                                                                              theorem pow_succ' {M : Type u_2} [Monoid M] (a : M) (n : ) :
                                                                                                              a ^ (n + 1) = a * a ^ n
                                                                                                              theorem succ_nsmul' {M : Type u_2} [AddMonoid M] (a : M) (n : ) :
                                                                                                              (n + 1) a = a + n a
                                                                                                              theorem pow_mul_comm' {M : Type u_2} [Monoid M] (a : M) (n : ) :
                                                                                                              a ^ n * a = a * a ^ n
                                                                                                              theorem nsmul_add_comm' {M : Type u_2} [AddMonoid M] (a : M) (n : ) :
                                                                                                              n a + a = a + n a
                                                                                                              theorem pow_two {M : Type u_2} [Monoid M] (a : M) :
                                                                                                              a ^ 2 = a * a

                                                                                                              Note that most of the lemmas about powers of two refer to it as sq.

                                                                                                              theorem two_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
                                                                                                              2 a = a + a
                                                                                                              theorem sq {M : Type u_2} [Monoid M] (a : M) :
                                                                                                              a ^ 2 = a * a

                                                                                                              Alias of pow_two.


                                                                                                              Note that most of the lemmas about powers of two refer to it as sq.

                                                                                                              theorem pow_three' {M : Type u_2} [Monoid M] (a : M) :
                                                                                                              a ^ 3 = a * a * a
                                                                                                              theorem three'_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
                                                                                                              3 a = a + a + a
                                                                                                              theorem pow_three {M : Type u_2} [Monoid M] (a : M) :
                                                                                                              a ^ 3 = a * (a * a)
                                                                                                              theorem three_nsmul {M : Type u_2} [AddMonoid M] (a : M) :
                                                                                                              3 a = a + (a + a)
                                                                                                              @[simp]
                                                                                                              theorem one_pow {M : Type u_2} [Monoid M] (n : ) :
                                                                                                              1 ^ n = 1
                                                                                                              theorem nsmul_zero {M : Type u_2} [AddMonoid M] (n : ) :
                                                                                                              n 0 = 0
                                                                                                              theorem pow_add {M : Type u_2} [Monoid M] (a : M) (m : ) (n : ) :
                                                                                                              a ^ (m + n) = a ^ m * a ^ n
                                                                                                              theorem add_nsmul {M : Type u_2} [AddMonoid M] (a : M) (m : ) (n : ) :
                                                                                                              (m + n) a = m a + n a
                                                                                                              theorem pow_mul_comm {M : Type u_2} [Monoid M] (a : M) (m : ) (n : ) :
                                                                                                              a ^ m * a ^ n = a ^ n * a ^ m
                                                                                                              theorem nsmul_add_comm {M : Type u_2} [AddMonoid M] (a : M) (m : ) (n : ) :
                                                                                                              m a + n a = n a + m a
                                                                                                              theorem pow_mul {M : Type u_2} [Monoid M] (a : M) (m : ) (n : ) :
                                                                                                              a ^ (m * n) = (a ^ m) ^ n
                                                                                                              theorem mul_nsmul {M : Type u_2} [AddMonoid M] (a : M) (m : ) (n : ) :
                                                                                                              (m * n) a = n m a
                                                                                                              theorem pow_mul' {M : Type u_2} [Monoid M] (a : M) (m : ) (n : ) :
                                                                                                              a ^ (m * n) = (a ^ n) ^ m
                                                                                                              theorem mul_nsmul' {M : Type u_2} [AddMonoid M] (a : M) (m : ) (n : ) :
                                                                                                              (m * n) a = m n a
                                                                                                              theorem pow_right_comm {M : Type u_2} [Monoid M] (a : M) (m : ) (n : ) :
                                                                                                              (a ^ m) ^ n = (a ^ n) ^ m
                                                                                                              theorem nsmul_left_comm {M : Type u_2} [AddMonoid M] (a : M) (m : ) (n : ) :
                                                                                                              n m a = m n a

                                                                                                              An additive commutative monoid is an additive monoid with commutative (+).

                                                                                                                Instances

                                                                                                                  A commutative monoid is a monoid with commutative (*).

                                                                                                                    Instances

                                                                                                                      An additive monoid in which addition is left-cancellative. Main examples are and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so AddLeftCancelSemigroup is not enough.

                                                                                                                        Instances

                                                                                                                          A monoid in which multiplication is left-cancellative.

                                                                                                                            Instances

                                                                                                                              An additive monoid in which addition is right-cancellative. Main examples are and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so AddRightCancelSemigroup is not enough.

                                                                                                                                Instances

                                                                                                                                  A monoid in which multiplication is right-cancellative.

                                                                                                                                    Instances

                                                                                                                                      An additive monoid in which addition is cancellative on both sides. Main examples are and groups. This is the right typeclass for many sum lemmas, as having a zero is useful to define the sum over the empty set, so AddRightCancelMonoid is not enough.

                                                                                                                                        Instances

                                                                                                                                          A monoid in which multiplication is cancellative.

                                                                                                                                            Instances
                                                                                                                                              @[instance 100]

                                                                                                                                              Any CancelMonoid G satisfies IsCancelMul G.

                                                                                                                                              Equations
                                                                                                                                              • =
                                                                                                                                              @[instance 100]

                                                                                                                                              Any AddCancelMonoid G satisfies IsCancelAdd G.

                                                                                                                                              Equations
                                                                                                                                              • =
                                                                                                                                              def zpowRec {G : Type u_1} [One G] [Mul G] [Inv G] (npow : optParam (GG) npowRec) :
                                                                                                                                              GG

                                                                                                                                              The fundamental power operation in a group. zpowRec n a = a*a*...*a n times, for integer n. Use instead a ^ n, which has better definitional behavior.

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                def zsmulRec {G : Type u_1} [Zero G] [Add G] [Neg G] (nsmul : optParam (GG) nsmulRec) :
                                                                                                                                                GG

                                                                                                                                                The fundamental scalar multiplication in an additive group. zpowRec n a = a+a+...+a n times, for integer n. Use instead n • a, which has better definitional behavior.

                                                                                                                                                Equations
                                                                                                                                                Instances For
                                                                                                                                                  class InvolutiveNeg (A : Type u_2) extends Neg :
                                                                                                                                                  Type u_2

                                                                                                                                                  Auxiliary typeclass for types with an involutive Neg.

                                                                                                                                                  • neg : AA
                                                                                                                                                  • neg_neg : ∀ (x : A), - -x = x
                                                                                                                                                  Instances
                                                                                                                                                    theorem InvolutiveNeg.neg_neg {A : Type u_2} [self : InvolutiveNeg A] (x : A) :
                                                                                                                                                    - -x = x
                                                                                                                                                    class InvolutiveInv (G : Type u_2) extends Inv :
                                                                                                                                                    Type u_2

                                                                                                                                                    Auxiliary typeclass for types with an involutive Inv.

                                                                                                                                                    Instances
                                                                                                                                                      theorem InvolutiveInv.inv_inv {G : Type u_2} [self : InvolutiveInv G] (x : G) :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem inv_inv {G : Type u_1} [InvolutiveInv G] (a : G) :
                                                                                                                                                      @[simp]
                                                                                                                                                      theorem neg_neg {G : Type u_1} [InvolutiveNeg G] (a : G) :
                                                                                                                                                      - -a = a

                                                                                                                                                      Design note on DivInvMonoid/SubNegMonoid and DivisionMonoid/SubtractionMonoid #

                                                                                                                                                      Those two pairs of made-up classes fulfill slightly different roles.

                                                                                                                                                      DivInvMonoid/SubNegMonoid provides the minimum amount of information to define the action (zpow or zsmul). Further, it provides a div field, matching the forgetful inheritance pattern. This is useful to shorten extension clauses of stronger structures (Group, GroupWithZero, DivisionRing, Field) and for a few structures with a rather weak pseudo-inverse (Matrix).

                                                                                                                                                      DivisionMonoid/SubtractionMonoid is targeted at structures with stronger pseudo-inverses. It is an ad hoc collection of axioms that are mainly respected by three things:

                                                                                                                                                      It acts as a middle ground for structures with an inversion operator that plays well with multiplication, except for the fact that it might not be a true inverse (a / a ≠ 1 in general). The axioms are pretty arbitrary (many other combinations are equivalent to it), but they are independent:

                                                                                                                                                      As a consequence, a few natural structures do not fit in this framework. For example, ENNReal respects everything except for the fact that (0 * ∞)⁻¹ = 0⁻¹ = ∞ while ∞⁻¹ * 0⁻¹ = 0 * ∞ = 0.

                                                                                                                                                      def DivInvMonoid.div' {G : Type u} [Monoid G] [Inv G] (a : G) (b : G) :
                                                                                                                                                      G

                                                                                                                                                      In a class equipped with instances of both Monoid and Inv, this definition records what the default definition for Div would be: a * b⁻¹. This is later provided as the default value for the Div instance in DivInvMonoid.

                                                                                                                                                      We keep it as a separate definition rather than inlining it in DivInvMonoid so that the Div field of individual DivInvMonoids constructed using that default value will not be unfolded at .instance transparency.

                                                                                                                                                      Equations
                                                                                                                                                      Instances For
                                                                                                                                                        class DivInvMonoid (G : Type u) extends Monoid , Inv , Div , Semigroup , MulOneClass , One , Mul :

                                                                                                                                                        A DivInvMonoid is a Monoid with operations / and ⁻¹ satisfying div_eq_mul_inv : ∀ a b, a / b = a * b⁻¹.

                                                                                                                                                        This deduplicates the name div_eq_mul_inv. The default for div is such that a / b = a * b⁻¹ holds by definition.

                                                                                                                                                        Adding div as a field rather than defining a / b := a * b⁻¹ allows us to avoid certain classes of unification failures, for example: Let Foo X be a type with a ∀ X, Div (Foo X) instance but no ∀ X, Inv (Foo X), e.g. when Foo X is a EuclideanDomain. Suppose we also have an instance ∀ X [Cromulent X], GroupWithZero (Foo X). Then the (/) coming from GroupWithZero.div cannot be definitionally equal to the (/) coming from Foo.Div.

                                                                                                                                                        In the same way, adding a zpow field makes it possible to avoid definitional failures in diamonds. See the definition of Monoid and Note [forgetful inheritance] for more explanations on this.

                                                                                                                                                        Instances
                                                                                                                                                          theorem DivInvMonoid.div_eq_mul_inv {G : Type u} [self : DivInvMonoid G] (a : G) (b : G) :
                                                                                                                                                          a / b = a * b⁻¹

                                                                                                                                                          a / b := a * b⁻¹

                                                                                                                                                          theorem DivInvMonoid.zpow_zero' {G : Type u} [self : DivInvMonoid G] (a : G) :

                                                                                                                                                          a ^ 0 = 1

                                                                                                                                                          theorem DivInvMonoid.zpow_succ' {G : Type u} [self : DivInvMonoid G] (n : ) (a : G) :
                                                                                                                                                          DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a

                                                                                                                                                          a ^ (n + 1) = a ^ n * a

                                                                                                                                                          theorem DivInvMonoid.zpow_neg' {G : Type u} [self : DivInvMonoid G] (n : ) (a : G) :

                                                                                                                                                          a ^ -(n + 1) = (a ^ (n + 1))⁻¹

                                                                                                                                                          def SubNegMonoid.sub' {G : Type u} [AddMonoid G] [Neg G] (a : G) (b : G) :
                                                                                                                                                          G

                                                                                                                                                          In a class equipped with instances of both AddMonoid and Neg, this definition records what the default definition for Sub would be: a + -b. This is later provided as the default value for the Sub instance in SubNegMonoid.

                                                                                                                                                          We keep it as a separate definition rather than inlining it in SubNegMonoid so that the Sub field of individual SubNegMonoids constructed using that default value will not be unfolded at .instance transparency.

                                                                                                                                                          Equations
                                                                                                                                                          Instances For
                                                                                                                                                            class SubNegMonoid (G : Type u) extends AddMonoid , Neg , Sub , AddSemigroup , AddZeroClass , Zero , Add :

                                                                                                                                                            A SubNegMonoid is an AddMonoid with unary - and binary - operations satisfying sub_eq_add_neg : ∀ a b, a - b = a + -b.

                                                                                                                                                            The default for sub is such that a - b = a + -b holds by definition.

                                                                                                                                                            Adding sub as a field rather than defining a - b := a + -b allows us to avoid certain classes of unification failures, for example: Let foo X be a type with a ∀ X, Sub (Foo X) instance but no ∀ X, Neg (Foo X). Suppose we also have an instance ∀ X [Cromulent X], AddGroup (Foo X). Then the (-) coming from AddGroup.sub cannot be definitionally equal to the (-) coming from Foo.Sub.

                                                                                                                                                            In the same way, adding a zsmul field makes it possible to avoid definitional failures in diamonds. See the definition of AddMonoid and Note [forgetful inheritance] for more explanations on this.

                                                                                                                                                            Instances
                                                                                                                                                              theorem SubNegMonoid.sub_eq_add_neg {G : Type u} [self : SubNegMonoid G] (a : G) (b : G) :
                                                                                                                                                              a - b = a + -b
                                                                                                                                                              theorem SubNegMonoid.zsmul_zero' {G : Type u} [self : SubNegMonoid G] (a : G) :
                                                                                                                                                              theorem SubNegMonoid.zsmul_succ' {G : Type u} [self : SubNegMonoid G] (n : ) (a : G) :
                                                                                                                                                              SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
                                                                                                                                                              theorem SubNegMonoid.zsmul_neg' {G : Type u} [self : SubNegMonoid G] (n : ) (a : G) :
                                                                                                                                                              instance DivInvMonoid.Pow {M : Type u_2} [DivInvMonoid M] :
                                                                                                                                                              Equations
                                                                                                                                                              instance SubNegMonoid.SMulInt {M : Type u_2} [SubNegMonoid M] :
                                                                                                                                                              Equations
                                                                                                                                                              • SubNegMonoid.SMulInt = { smul := SubNegMonoid.zsmul }
                                                                                                                                                              class IsAddCyclic (G : Type u) [SMul G] :

                                                                                                                                                              A group is called cyclic if it is generated by a single element.

                                                                                                                                                              Instances
                                                                                                                                                                theorem IsAddCyclic.exists_zsmul_surjective {G : Type u} :
                                                                                                                                                                ∀ {inst : SMul G} [self : IsAddCyclic G], ∃ (g : G), Function.Surjective fun (x : ) => x g
                                                                                                                                                                class IsCyclic (G : Type u) [Pow G ] :

                                                                                                                                                                A group is called cyclic if it is generated by a single element.

                                                                                                                                                                Instances
                                                                                                                                                                  theorem IsCyclic.exists_zpow_surjective {G : Type u} :
                                                                                                                                                                  ∀ {inst : Pow G } [self : IsCyclic G], ∃ (g : G), Function.Surjective fun (x : ) => g ^ x
                                                                                                                                                                  theorem exists_zpow_surjective (G : Type u_2) [Pow G ] [IsCyclic G] :
                                                                                                                                                                  ∃ (g : G), Function.Surjective fun (x : ) => g ^ x
                                                                                                                                                                  theorem exists_zsmul_surjective (G : Type u_2) [SMul G] [IsAddCyclic G] :
                                                                                                                                                                  ∃ (g : G), Function.Surjective fun (x : ) => x g
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem zpow_eq_pow {G : Type u_1} [DivInvMonoid G] (n : ) (x : G) :
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem zsmul_eq_smul {G : Type u_1} [SubNegMonoid G] (n : ) (x : G) :
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem zpow_zero {G : Type u_1} [DivInvMonoid G] (a : G) :
                                                                                                                                                                  a ^ 0 = 1
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem zero_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) :
                                                                                                                                                                  0 a = 0
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem zpow_natCast {G : Type u_1} [DivInvMonoid G] (a : G) (n : ) :
                                                                                                                                                                  a ^ n = a ^ n
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem natCast_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ) :
                                                                                                                                                                  n a = n a
                                                                                                                                                                  @[deprecated zpow_natCast]
                                                                                                                                                                  theorem zpow_coe_nat {G : Type u_1} [DivInvMonoid G] (a : G) (n : ) :
                                                                                                                                                                  a ^ n = a ^ n

                                                                                                                                                                  Alias of zpow_natCast.

                                                                                                                                                                  @[deprecated natCast_zsmul]
                                                                                                                                                                  theorem coe_nat_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ) :
                                                                                                                                                                  n a = n a

                                                                                                                                                                  Alias of natCast_zsmul.

                                                                                                                                                                  theorem zpow_ofNat {G : Type u_1} [DivInvMonoid G] (a : G) (n : ) :
                                                                                                                                                                  theorem ofNat_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) (n : ) :
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem zpow_negSucc {G : Type u_1} [DivInvMonoid G] (a : G) (n : ) :
                                                                                                                                                                  a ^ Int.negSucc n = (a ^ (n + 1))⁻¹
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem negSucc_zsmul {G : Type u_2} [SubNegMonoid G] (a : G) (n : ) :
                                                                                                                                                                  Int.negSucc n a = -((n + 1) a)
                                                                                                                                                                  theorem div_eq_mul_inv {G : Type u_1} [DivInvMonoid G] (a : G) (b : G) :
                                                                                                                                                                  a / b = a * b⁻¹

                                                                                                                                                                  Dividing by an element is the same as multiplying by its inverse.

                                                                                                                                                                  This is a duplicate of DivInvMonoid.div_eq_mul_inv ensuring that the types unfold better.

                                                                                                                                                                  theorem sub_eq_add_neg {G : Type u_1} [SubNegMonoid G] (a : G) (b : G) :
                                                                                                                                                                  a - b = a + -b

                                                                                                                                                                  Subtracting an element is the same as adding by its negative. This is a duplicate of SubNegMonoid.sub_eq_mul_neg ensuring that the types unfold better.

                                                                                                                                                                  theorem division_def {G : Type u_1} [DivInvMonoid G] (a : G) (b : G) :
                                                                                                                                                                  a / b = a * b⁻¹

                                                                                                                                                                  Alias of div_eq_mul_inv.


                                                                                                                                                                  Dividing by an element is the same as multiplying by its inverse.

                                                                                                                                                                  This is a duplicate of DivInvMonoid.div_eq_mul_inv ensuring that the types unfold better.

                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem zpow_one {G : Type u_1} [DivInvMonoid G] (a : G) :
                                                                                                                                                                  a ^ 1 = a
                                                                                                                                                                  @[simp]
                                                                                                                                                                  theorem one_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) :
                                                                                                                                                                  1 a = a
                                                                                                                                                                  theorem zpow_two {G : Type u_1} [DivInvMonoid G] (a : G) :
                                                                                                                                                                  a ^ 2 = a * a
                                                                                                                                                                  theorem two_zsmul {G : Type u_1} [SubNegMonoid G] (a : G) :
                                                                                                                                                                  2 a = a + a
                                                                                                                                                                  theorem zpow_neg_one {G : Type u_1} [DivInvMonoid G] (x : G) :
                                                                                                                                                                  x ^ (-1) = x⁻¹
                                                                                                                                                                  theorem neg_one_zsmul {G : Type u_1} [SubNegMonoid G] (x : G) :
                                                                                                                                                                  -1 x = -x
                                                                                                                                                                  theorem zpow_neg_coe_of_pos {G : Type u_1} [DivInvMonoid G] (a : G) {n : } :
                                                                                                                                                                  0 < na ^ (-n) = (a ^ n)⁻¹
                                                                                                                                                                  theorem zsmul_neg_coe_of_pos {G : Type u_1} [SubNegMonoid G] (a : G) {n : } :
                                                                                                                                                                  0 < n-n a = -(n a)
                                                                                                                                                                  class NegZeroClass (G : Type u_2) extends Zero , Neg :
                                                                                                                                                                  Type u_2

                                                                                                                                                                  Typeclass for expressing that -0 = 0.

                                                                                                                                                                  • zero : G
                                                                                                                                                                  • neg : GG
                                                                                                                                                                  • neg_zero : -0 = 0
                                                                                                                                                                  Instances
                                                                                                                                                                    theorem NegZeroClass.neg_zero {G : Type u_2} [self : NegZeroClass G] :
                                                                                                                                                                    -0 = 0

                                                                                                                                                                    A SubNegMonoid where -0 = 0.

                                                                                                                                                                      Instances
                                                                                                                                                                        class InvOneClass (G : Type u_2) extends One , Inv :
                                                                                                                                                                        Type u_2

                                                                                                                                                                        Typeclass for expressing that 1⁻¹ = 1.

                                                                                                                                                                        • one : G
                                                                                                                                                                        • inv : GG
                                                                                                                                                                        • inv_one : 1⁻¹ = 1
                                                                                                                                                                        Instances
                                                                                                                                                                          theorem InvOneClass.inv_one {G : Type u_2} [self : InvOneClass G] :
                                                                                                                                                                          1⁻¹ = 1
                                                                                                                                                                          class DivInvOneMonoid (G : Type u_2) extends DivInvMonoid , InvOneClass , Monoid , Inv , Div , Semigroup , MulOneClass , One , Mul :
                                                                                                                                                                          Type u_2

                                                                                                                                                                          A DivInvMonoid where 1⁻¹ = 1.

                                                                                                                                                                            Instances
                                                                                                                                                                              @[simp]
                                                                                                                                                                              theorem inv_one {G : Type u_1} [InvOneClass G] :
                                                                                                                                                                              1⁻¹ = 1
                                                                                                                                                                              @[simp]
                                                                                                                                                                              theorem neg_zero {G : Type u_1} [NegZeroClass G] :
                                                                                                                                                                              -0 = 0

                                                                                                                                                                              A SubtractionMonoid is a SubNegMonoid with involutive negation and such that -(a + b) = -b + -a and a + b = 0 → -a = b.

                                                                                                                                                                                Instances
                                                                                                                                                                                  theorem SubtractionMonoid.neg_add_rev {G : Type u} [self : SubtractionMonoid G] (a : G) (b : G) :
                                                                                                                                                                                  -(a + b) = -b + -a
                                                                                                                                                                                  theorem SubtractionMonoid.neg_eq_of_add {G : Type u} [self : SubtractionMonoid G] (a : G) (b : G) :
                                                                                                                                                                                  a + b = 0-a = b

                                                                                                                                                                                  Despite the asymmetry of neg_eq_of_add, the symmetric version is true thanks to the involutivity of negation.

                                                                                                                                                                                  A DivisionMonoid is a DivInvMonoid with involutive inversion and such that (a * b)⁻¹ = b⁻¹ * a⁻¹ and a * b = 1 → a⁻¹ = b.

                                                                                                                                                                                  This is the immediate common ancestor of Group and GroupWithZero.

                                                                                                                                                                                    Instances
                                                                                                                                                                                      theorem DivisionMonoid.mul_inv_rev {G : Type u} [self : DivisionMonoid G] (a : G) (b : G) :
                                                                                                                                                                                      (a * b)⁻¹ = b⁻¹ * a⁻¹
                                                                                                                                                                                      theorem DivisionMonoid.inv_eq_of_mul {G : Type u} [self : DivisionMonoid G] (a : G) (b : G) :
                                                                                                                                                                                      a * b = 1a⁻¹ = b

                                                                                                                                                                                      Despite the asymmetry of inv_eq_of_mul, the symmetric version is true thanks to the involutivity of inversion.

                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem mul_inv_rev {G : Type u_1} [DivisionMonoid G] (a : G) (b : G) :
                                                                                                                                                                                      (a * b)⁻¹ = b⁻¹ * a⁻¹
                                                                                                                                                                                      @[simp]
                                                                                                                                                                                      theorem neg_add_rev {G : Type u_1} [SubtractionMonoid G] (a : G) (b : G) :
                                                                                                                                                                                      -(a + b) = -b + -a
                                                                                                                                                                                      theorem inv_eq_of_mul_eq_one_right {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} :
                                                                                                                                                                                      a * b = 1a⁻¹ = b
                                                                                                                                                                                      theorem neg_eq_of_add_eq_zero_right {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} :
                                                                                                                                                                                      a + b = 0-a = b
                                                                                                                                                                                      theorem inv_eq_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (h : a * b = 1) :
                                                                                                                                                                                      b⁻¹ = a
                                                                                                                                                                                      theorem neg_eq_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (h : a + b = 0) :
                                                                                                                                                                                      -b = a
                                                                                                                                                                                      theorem eq_inv_of_mul_eq_one_left {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (h : a * b = 1) :
                                                                                                                                                                                      a = b⁻¹
                                                                                                                                                                                      theorem eq_neg_of_add_eq_zero_left {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (h : a + b = 0) :
                                                                                                                                                                                      a = -b

                                                                                                                                                                                      Commutative DivisionMonoid.

                                                                                                                                                                                      This is the immediate common ancestor of CommGroup and CommGroupWithZero.

                                                                                                                                                                                        Instances
                                                                                                                                                                                          class Group (G : Type u) extends DivInvMonoid , Monoid , Inv , Div , Semigroup , MulOneClass , One , Mul :

                                                                                                                                                                                          A Group is a Monoid with an operation ⁻¹ satisfying a⁻¹ * a = 1.

                                                                                                                                                                                          There is also a division operation / such that a / b = a * b⁻¹, with a default so that a / b = a * b⁻¹ holds by definition.

                                                                                                                                                                                          Use Group.ofLeftAxioms or Group.ofRightAxioms to define a group structure on a type with the minimum proof obligations.

                                                                                                                                                                                            Instances
                                                                                                                                                                                              theorem Group.inv_mul_cancel {G : Type u} [self : Group G] (a : G) :
                                                                                                                                                                                              a⁻¹ * a = 1

                                                                                                                                                                                              An AddGroup is an AddMonoid with a unary - satisfying -a + a = 0.

                                                                                                                                                                                              There is also a binary operation - such that a - b = a + -b, with a default so that a - b = a + -b holds by definition.

                                                                                                                                                                                              Use AddGroup.ofLeftAxioms or AddGroup.ofRightAxioms to define an additive group structure on a type with the minimum proof obligations.

                                                                                                                                                                                                Instances
                                                                                                                                                                                                  theorem AddGroup.neg_add_cancel {A : Type u} [self : AddGroup A] (a : A) :
                                                                                                                                                                                                  -a + a = 0
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem inv_mul_cancel {G : Type u_1} [Group G] (a : G) :
                                                                                                                                                                                                  a⁻¹ * a = 1
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem neg_add_cancel {G : Type u_1} [AddGroup G] (a : G) :
                                                                                                                                                                                                  -a + a = 0
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem mul_inv_cancel {G : Type u_1} [Group G] (a : G) :
                                                                                                                                                                                                  a * a⁻¹ = 1
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem add_neg_cancel {G : Type u_1} [AddGroup G] (a : G) :
                                                                                                                                                                                                  a + -a = 0
                                                                                                                                                                                                  @[deprecated inv_mul_cancel]
                                                                                                                                                                                                  theorem mul_left_inv {G : Type u_1} [Group G] (a : G) :
                                                                                                                                                                                                  a⁻¹ * a = 1

                                                                                                                                                                                                  Alias of inv_mul_cancel.

                                                                                                                                                                                                  @[deprecated mul_inv_cancel]
                                                                                                                                                                                                  theorem mul_right_inv {G : Type u_1} [Group G] (a : G) :
                                                                                                                                                                                                  a * a⁻¹ = 1

                                                                                                                                                                                                  Alias of mul_inv_cancel.

                                                                                                                                                                                                  @[deprecated neg_add_cancel]
                                                                                                                                                                                                  theorem add_left_neg {G : Type u_1} [AddGroup G] (a : G) :
                                                                                                                                                                                                  -a + a = 0

                                                                                                                                                                                                  Alias of neg_add_cancel.

                                                                                                                                                                                                  @[deprecated add_neg_cancel]
                                                                                                                                                                                                  theorem add_right_neg {G : Type u_1} [AddGroup G] (a : G) :
                                                                                                                                                                                                  a + -a = 0

                                                                                                                                                                                                  Alias of add_neg_cancel.

                                                                                                                                                                                                  @[deprecated inv_mul_cancel]
                                                                                                                                                                                                  theorem inv_mul_self {G : Type u_1} [Group G] (a : G) :
                                                                                                                                                                                                  a⁻¹ * a = 1

                                                                                                                                                                                                  Alias of inv_mul_cancel.

                                                                                                                                                                                                  @[deprecated mul_inv_cancel]
                                                                                                                                                                                                  theorem mul_inv_self {G : Type u_1} [Group G] (a : G) :
                                                                                                                                                                                                  a * a⁻¹ = 1

                                                                                                                                                                                                  Alias of mul_inv_cancel.

                                                                                                                                                                                                  @[deprecated neg_add_cancel]
                                                                                                                                                                                                  theorem neg_add_self {G : Type u_1} [AddGroup G] (a : G) :
                                                                                                                                                                                                  -a + a = 0

                                                                                                                                                                                                  Alias of neg_add_cancel.

                                                                                                                                                                                                  @[deprecated add_neg_cancel]
                                                                                                                                                                                                  theorem add_right_self {G : Type u_1} [AddGroup G] (a : G) :
                                                                                                                                                                                                  a + -a = 0

                                                                                                                                                                                                  Alias of add_neg_cancel.

                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem inv_mul_cancel_left {G : Type u_1} [Group G] (a : G) (b : G) :
                                                                                                                                                                                                  a⁻¹ * (a * b) = b
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem neg_add_cancel_left {G : Type u_1} [AddGroup G] (a : G) (b : G) :
                                                                                                                                                                                                  -a + (a + b) = b
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem mul_inv_cancel_left {G : Type u_1} [Group G] (a : G) (b : G) :
                                                                                                                                                                                                  a * (a⁻¹ * b) = b
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem add_neg_cancel_left {G : Type u_1} [AddGroup G] (a : G) (b : G) :
                                                                                                                                                                                                  a + (-a + b) = b
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem mul_inv_cancel_right {G : Type u_1} [Group G] (a : G) (b : G) :
                                                                                                                                                                                                  a * b * b⁻¹ = a
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem add_neg_cancel_right {G : Type u_1} [AddGroup G] (a : G) (b : G) :
                                                                                                                                                                                                  a + b + -b = a
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem inv_mul_cancel_right {G : Type u_1} [Group G] (a : G) (b : G) :
                                                                                                                                                                                                  a * b⁻¹ * b = a
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem neg_add_cancel_right {G : Type u_1} [AddGroup G] (a : G) (b : G) :
                                                                                                                                                                                                  a + -b + b = a
                                                                                                                                                                                                  @[instance 100]
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  @[instance 100]
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  @[instance 100]
                                                                                                                                                                                                  instance Group.toCancelMonoid {G : Type u_1} [Group G] :
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  @[instance 100]
                                                                                                                                                                                                  Equations

                                                                                                                                                                                                  An additive commutative group is an additive group with commutative (+).

                                                                                                                                                                                                    Instances

                                                                                                                                                                                                      A commutative group is a group with commutative (*).

                                                                                                                                                                                                        Instances
                                                                                                                                                                                                          @[instance 100]
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          @[instance 100]
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          @[instance 100]
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          @[instance 100]
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem inv_mul_cancel_comm {G : Type u_1} [CommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          a⁻¹ * b * a = b
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem neg_add_cancel_comm {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          -a + b + a = b
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem mul_inv_cancel_comm {G : Type u_1} [CommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          a * b * a⁻¹ = b
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem add_neg_cancel_comm {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          a + b + -a = b
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem inv_mul_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          a⁻¹ * (b * a) = b
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem neg_add_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          -a + (b + a) = b
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem mul_inv_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          a * (b * a⁻¹) = b
                                                                                                                                                                                                          @[simp]
                                                                                                                                                                                                          theorem add_neg_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :
                                                                                                                                                                                                          a + (b + -a) = b

                                                                                                                                                                                                          We initialize all projections for @[simps] here, so that we don't have to do it in later files.

                                                                                                                                                                                                          Note: the lemmas generated for the npow/zpow projections will not apply to x ^ y, since the argument order of these projections doesn't match the argument order of ^. The nsmul/zsmul lemmas will be correct.