Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

source
instance MulOpposite.instAddSemigroup {α : Type u_1} [AddSemigroup α] :
AddSemigroup αᵐᵒᵖ
Equations
    source
    instance MulOpposite.instAddLeftCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :
    AddLeftCancelSemigroup αᵐᵒᵖ
    Equations
      source
      instance MulOpposite.instAddRightCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :
      AddRightCancelSemigroup αᵐᵒᵖ
      Equations
        source
        instance MulOpposite.instAddCommMagma {α : Type u_1} [AddCommMagma α] :
        AddCommMagma αᵐᵒᵖ
        Equations
          source
          instance MulOpposite.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :
          AddCommSemigroup αᵐᵒᵖ
          Equations
            source
            instance MulOpposite.instAddZeroClass {α : Type u_1} [AddZeroClass α] :
            AddZeroClass αᵐᵒᵖ
            Equations
              source
              instance MulOpposite.instAddMonoid {α : Type u_1} [AddMonoid α] :
              AddMonoid αᵐᵒᵖ
              Equations
                source
                instance MulOpposite.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :
                AddCommMonoid αᵐᵒᵖ
                Equations
                  source
                  instance MulOpposite.instSubNegMonoid {α : Type u_1} [SubNegMonoid α] :
                  SubNegMonoid αᵐᵒᵖ
                  Equations
                    source
                    instance MulOpposite.instAddGroup {α : Type u_1} [AddGroup α] :
                    AddGroup αᵐᵒᵖ
                    Equations
                      source
                      instance MulOpposite.instAddCommGroup {α : Type u_1} [AddCommGroup α] :
                      AddCommGroup αᵐᵒᵖ
                      Equations

                        Multiplicative structures on αᵐᵒᵖ #

                        We also generate additive structures on αᵃᵒᵖ using to_additive

                        source
                        instance MulOpposite.instIsRightCancelMul {α : Type u_1} [Mul α] [IsLeftCancelMul α] :
                        IsRightCancelMul αᵐᵒᵖ
                        source
                        instance AddOpposite.instIsRightCancelAdd {α : Type u_1} [Add α] [IsLeftCancelAdd α] :
                        IsRightCancelAdd αᵃᵒᵖ
                        source
                        instance MulOpposite.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] :
                        IsLeftCancelMul αᵐᵒᵖ
                        source
                        instance AddOpposite.instIsLeftCancelAdd {α : Type u_1} [Add α] [IsRightCancelAdd α] :
                        IsLeftCancelAdd αᵃᵒᵖ
                        source
                        instance MulOpposite.instSemigroup {α : Type u_1} [Semigroup α] :
                        Semigroup αᵐᵒᵖ
                        Equations
                          source
                          instance AddOpposite.instAddSemigroup {α : Type u_1} [AddSemigroup α] :
                          AddSemigroup αᵃᵒᵖ
                          Equations
                            source
                            instance MulOpposite.instLeftCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :
                            LeftCancelSemigroup αᵐᵒᵖ
                            Equations
                              source
                              instance AddOpposite.instAddLeftCancelSemigroup {α : Type u_1} [AddRightCancelSemigroup α] :
                              AddLeftCancelSemigroup αᵃᵒᵖ
                              Equations
                                source
                                instance MulOpposite.instRightCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :
                                RightCancelSemigroup αᵐᵒᵖ
                                Equations
                                  source
                                  instance AddOpposite.instAddRightCancelSemigroup {α : Type u_1} [AddLeftCancelSemigroup α] :
                                  AddRightCancelSemigroup αᵃᵒᵖ
                                  Equations
                                    source
                                    instance MulOpposite.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
                                    CommSemigroup αᵐᵒᵖ
                                    Equations
                                      source
                                      instance AddOpposite.instAddCommSemigroup {α : Type u_1} [AddCommSemigroup α] :
                                      AddCommSemigroup αᵃᵒᵖ
                                      Equations
                                        source
                                        instance MulOpposite.instMulOneClass {α : Type u_1} [MulOneClass α] :
                                        MulOneClass αᵐᵒᵖ
                                        Equations
                                          source
                                          instance AddOpposite.instAddZeroClass {α : Type u_1} [AddZeroClass α] :
                                          AddZeroClass αᵃᵒᵖ
                                          Equations
                                            source
                                            instance MulOpposite.instMonoid {α : Type u_1} [Monoid α] :
                                            Monoid αᵐᵒᵖ
                                            Equations
                                              source
                                              instance AddOpposite.instAddMonoid {α : Type u_1} [AddMonoid α] :
                                              AddMonoid αᵃᵒᵖ
                                              Equations
                                                source
                                                instance MulOpposite.instLeftCancelMonoid {α : Type u_1} [RightCancelMonoid α] :
                                                LeftCancelMonoid αᵐᵒᵖ
                                                Equations
                                                  source
                                                  instance AddOpposite.instAddLeftCancelMonoid {α : Type u_1} [AddRightCancelMonoid α] :
                                                  AddLeftCancelMonoid αᵃᵒᵖ
                                                  Equations
                                                    source
                                                    instance MulOpposite.instRightCancelMonoid {α : Type u_1} [LeftCancelMonoid α] :
                                                    RightCancelMonoid αᵐᵒᵖ
                                                    Equations
                                                      source
                                                      instance AddOpposite.instAddRightCancelMonoid {α : Type u_1} [AddLeftCancelMonoid α] :
                                                      AddRightCancelMonoid αᵃᵒᵖ
                                                      Equations
                                                        source
                                                        instance MulOpposite.instCancelMonoid {α : Type u_1} [CancelMonoid α] :
                                                        CancelMonoid αᵐᵒᵖ
                                                        Equations
                                                          source
                                                          instance AddOpposite.instAddCancelMonoid {α : Type u_1} [AddCancelMonoid α] :
                                                          AddCancelMonoid αᵃᵒᵖ
                                                          Equations
                                                            source
                                                            instance MulOpposite.instCommMonoid {α : Type u_1} [CommMonoid α] :
                                                            CommMonoid αᵐᵒᵖ
                                                            Equations
                                                              source
                                                              instance AddOpposite.instAddCommMonoid {α : Type u_1} [AddCommMonoid α] :
                                                              AddCommMonoid αᵃᵒᵖ
                                                              Equations
                                                                source
                                                                instance MulOpposite.instCancelCommMonoid {α : Type u_1} [CancelCommMonoid α] :
                                                                CancelCommMonoid αᵐᵒᵖ
                                                                Equations
                                                                  source
                                                                  instance AddOpposite.instAddCancelCommMonoid {α : Type u_1} [AddCancelCommMonoid α] :
                                                                  AddCancelCommMonoid αᵃᵒᵖ
                                                                  Equations
                                                                    source
                                                                    instance MulOpposite.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :
                                                                    DivInvMonoid αᵐᵒᵖ
                                                                    Equations
                                                                      source
                                                                      instance AddOpposite.instSubNegMonoid {α : Type u_1} [SubNegMonoid α] :
                                                                      SubNegMonoid αᵃᵒᵖ
                                                                      Equations
                                                                        source
                                                                        instance MulOpposite.instDivisionMonoid {α : Type u_1} [DivisionMonoid α] :
                                                                        DivisionMonoid αᵐᵒᵖ
                                                                        Equations
                                                                          source
                                                                          instance AddOpposite.instSubtractionMonoid {α : Type u_1} [SubtractionMonoid α] :
                                                                          SubtractionMonoid αᵃᵒᵖ
                                                                          Equations
                                                                            source
                                                                            instance MulOpposite.instDivisionCommMonoid {α : Type u_1} [DivisionCommMonoid α] :
                                                                            DivisionCommMonoid αᵐᵒᵖ
                                                                            Equations
                                                                              source
                                                                              instance AddOpposite.instSubtractionCommMonoid {α : Type u_1} [SubtractionCommMonoid α] :
                                                                              SubtractionCommMonoid αᵃᵒᵖ
                                                                              Equations
                                                                                source
                                                                                instance MulOpposite.instGroup {α : Type u_1} [Group α] :
                                                                                Group αᵐᵒᵖ
                                                                                Equations
                                                                                  source
                                                                                  instance AddOpposite.instAddGroup {α : Type u_1} [AddGroup α] :
                                                                                  AddGroup αᵃᵒᵖ
                                                                                  Equations
                                                                                    source
                                                                                    instance MulOpposite.instCommGroup {α : Type u_1} [CommGroup α] :
                                                                                    CommGroup αᵐᵒᵖ
                                                                                    Equations
                                                                                      source
                                                                                      instance AddOpposite.instAddCommGroup {α : Type u_1} [AddCommGroup α] :
                                                                                      AddCommGroup αᵃᵒᵖ
                                                                                      Equations
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.op_pow {α : Type u_1} [Monoid α] (x : α) (n : ℕ) :
                                                                                        op (x ^ n) = op x ^ n
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.unop_pow {α : Type u_1} [Monoid α] (x : αᵐᵒᵖ) (n : ℕ) :
                                                                                        unop (x ^ n) = unop x ^ n
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.op_zpow {α : Type u_1} [DivInvMonoid α] (x : α) (z : ℤ) :
                                                                                        op (x ^ z) = op x ^ z
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.unop_zpow {α : Type u_1} [DivInvMonoid α] (x : αᵐᵒᵖ) (z : ℤ) :
                                                                                        unop (x ^ z) = unop x ^ z
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.unop_div {α : Type u_1} [DivInvMonoid α] (x y : αᵐᵒᵖ) :
                                                                                        unop (x / y) = (unop y)⁻¹ * unop x
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem AddOpposite.unop_sub {α : Type u_1} [SubNegMonoid α] (x y : αᵃᵒᵖ) :
                                                                                        unop (x - y) = -unop y + unop x
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.op_div {α : Type u_1} [DivInvMonoid α] (x y : α) :
                                                                                        op (x / y) = (op y)⁻¹ * op x
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem AddOpposite.op_sub {α : Type u_1} [SubNegMonoid α] (x y : α) :
                                                                                        op (x - y) = -op y + op x
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.semiconjBy_op {α : Type u_1} [Mul α] {a x y : α} :
                                                                                        SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem AddOpposite.addSemiconjBy_op {α : Type u_1} [Add α] {a x y : α} :
                                                                                        AddSemiconjBy (op a) (op y) (op x) ↔ AddSemiconjBy a x y
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.semiconjBy_unop {α : Type u_1} [Mul α] {a x y : αᵐᵒᵖ} :
                                                                                        SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem AddOpposite.addSemiconjBy_unop {α : Type u_1} [Add α] {a x y : αᵃᵒᵖ} :
                                                                                        AddSemiconjBy (unop a) (unop y) (unop x) ↔ AddSemiconjBy a x y
                                                                                        source
                                                                                        theorem SemiconjBy.op {α : Type u_1} [Mul α] {a x y : α} (h : SemiconjBy a x y) :
                                                                                        SemiconjBy (MulOpposite.op a) (MulOpposite.op y) (MulOpposite.op x)
                                                                                        source
                                                                                        theorem AddSemiconjBy.op {α : Type u_1} [Add α] {a x y : α} (h : AddSemiconjBy a x y) :
                                                                                        AddSemiconjBy (AddOpposite.op a) (AddOpposite.op y) (AddOpposite.op x)
                                                                                        source
                                                                                        theorem SemiconjBy.unop {α : Type u_1} [Mul α] {a x y : αᵐᵒᵖ} (h : SemiconjBy a x y) :
                                                                                        SemiconjBy (MulOpposite.unop a) (MulOpposite.unop y) (MulOpposite.unop x)
                                                                                        source
                                                                                        theorem AddSemiconjBy.unop {α : Type u_1} [Add α] {a x y : αᵃᵒᵖ} (h : AddSemiconjBy a x y) :
                                                                                        AddSemiconjBy (AddOpposite.unop a) (AddOpposite.unop y) (AddOpposite.unop x)
                                                                                        source
                                                                                        theorem Commute.op {α : Type u_1} [Mul α] {x y : α} (h : Commute x y) :
                                                                                        Commute (MulOpposite.op x) (MulOpposite.op y)
                                                                                        source
                                                                                        theorem AddCommute.op {α : Type u_1} [Add α] {x y : α} (h : AddCommute x y) :
                                                                                        AddCommute (AddOpposite.op x) (AddOpposite.op y)
                                                                                        source
                                                                                        theorem Commute.unop {α : Type u_1} [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) :
                                                                                        Commute (MulOpposite.unop x) (MulOpposite.unop y)
                                                                                        source
                                                                                        theorem AddCommute.unop {α : Type u_1} [Add α] {x y : αᵃᵒᵖ} (h : AddCommute x y) :
                                                                                        AddCommute (AddOpposite.unop x) (AddOpposite.unop y)
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.commute_op {α : Type u_1} [Mul α] {x y : α} :
                                                                                        Commute (op x) (op y) ↔ Commute x y
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem AddOpposite.addCommute_op {α : Type u_1} [Add α] {x y : α} :
                                                                                        AddCommute (op x) (op y) ↔ AddCommute x y
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem MulOpposite.commute_unop {α : Type u_1} [Mul α] {x y : αᵐᵒᵖ} :
                                                                                        Commute (unop x) (unop y) ↔ Commute x y
                                                                                        source
                                                                                        @[simp]
                                                                                        theorem AddOpposite.addCommute_unop {α : Type u_1} [Add α] {x y : αᵃᵒᵖ} :
                                                                                        AddCommute (unop x) (unop y) ↔ AddCommute x y

                                                                                        Multiplicative structures on αᵃᵒᵖ #

                                                                                        source
                                                                                        instance AddOpposite.instSemigroup {α : Type u_1} [Semigroup α] :
                                                                                        Semigroup αᵃᵒᵖ
                                                                                        Equations
                                                                                          source
                                                                                          instance AddOpposite.instLeftCancelSemigroup {α : Type u_1} [LeftCancelSemigroup α] :
                                                                                          LeftCancelSemigroup αᵃᵒᵖ
                                                                                          Equations
                                                                                            source
                                                                                            instance AddOpposite.instRightCancelSemigroup {α : Type u_1} [RightCancelSemigroup α] :
                                                                                            RightCancelSemigroup αᵃᵒᵖ
                                                                                            Equations
                                                                                              source
                                                                                              instance AddOpposite.instCommSemigroup {α : Type u_1} [CommSemigroup α] :
                                                                                              CommSemigroup αᵃᵒᵖ
                                                                                              Equations
                                                                                                source
                                                                                                instance AddOpposite.instMulOneClass {α : Type u_1} [MulOneClass α] :
                                                                                                MulOneClass αᵃᵒᵖ
                                                                                                Equations
                                                                                                  source
                                                                                                  instance AddOpposite.pow {α : Type u_1} {β : Type u_2} [Pow α β] :
                                                                                                  Pow αᵃᵒᵖ β
                                                                                                  Equations
                                                                                                    source
                                                                                                    @[simp]
                                                                                                    theorem AddOpposite.op_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
                                                                                                    op (a ^ b) = op a ^ b
                                                                                                    source
                                                                                                    @[simp]
                                                                                                    theorem AddOpposite.unop_pow {α : Type u_1} {β : Type u_2} [Pow α β] (a : αᵃᵒᵖ) (b : β) :
                                                                                                    unop (a ^ b) = unop a ^ b
                                                                                                    source
                                                                                                    instance AddOpposite.instMonoid {α : Type u_1} [Monoid α] :
                                                                                                    Monoid αᵃᵒᵖ
                                                                                                    Equations
                                                                                                      source
                                                                                                      instance AddOpposite.instCommMonoid {α : Type u_1} [CommMonoid α] :
                                                                                                      CommMonoid αᵃᵒᵖ
                                                                                                      Equations
                                                                                                        source
                                                                                                        instance AddOpposite.instDivInvMonoid {α : Type u_1} [DivInvMonoid α] :
                                                                                                        DivInvMonoid αᵃᵒᵖ
                                                                                                        Equations
                                                                                                          source
                                                                                                          instance AddOpposite.instGroup {α : Type u_1} [Group α] :
                                                                                                          Group αᵃᵒᵖ
                                                                                                          Equations
                                                                                                            source
                                                                                                            instance AddOpposite.instCommGroup {α : Type u_1} [CommGroup α] :
                                                                                                            CommGroup αᵃᵒᵖ
                                                                                                            Equations