Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

source
instance MulOpposite.instNatCast {α : Type u_1} [NatCast α] :
NatCast αᵐᵒᵖ
Equations
    source
    instance AddOpposite.instNatCast {α : Type u_1} [NatCast α] :
    NatCast αᵃᵒᵖ
    Equations
      source
      instance MulOpposite.instIntCast {α : Type u_1} [IntCast α] :
      IntCast αᵐᵒᵖ
      Equations
        source
        instance AddOpposite.instIntCast {α : Type u_1} [IntCast α] :
        IntCast αᵃᵒᵖ
        Equations
          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.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.instAddMonoidWithOne {α : Type u_1} [AddMonoidWithOne α] :
                        AddMonoidWithOne αᵐᵒᵖ
                        Equations
                          source
                          instance MulOpposite.instAddCommMonoidWithOne {α : Type u_1} [AddCommMonoidWithOne α] :
                          AddCommMonoidWithOne αᵐᵒᵖ
                          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
                                  source
                                  instance MulOpposite.instAddGroupWithOne {α : Type u_1} [AddGroupWithOne α] :
                                  AddGroupWithOne αᵐᵒᵖ
                                  Equations
                                    source
                                    instance MulOpposite.instAddCommGroupWithOne {α : Type u_1} [AddCommGroupWithOne α] :
                                    AddCommGroupWithOne αᵐᵒᵖ
                                    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.instIsAddRightCancel {α : Type u_1} [Add α] [IsLeftCancelAdd α] :
                                      IsRightCancelAdd αᵃᵒᵖ
                                      source
                                      instance MulOpposite.instIsLeftCancelMul {α : Type u_1} [Mul α] [IsRightCancelMul α] :
                                      IsLeftCancelMul αᵐᵒᵖ
                                      source
                                      instance AddOpposite.instIsAddLeftCancel {α : 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.op_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
                                                                                                      op ↑n = ↑n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem AddOpposite.op_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
                                                                                                      op ↑n = ↑n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem MulOpposite.op_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
                                                                                                      op (OfNat.ofNat n) = OfNat.ofNat n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem AddOpposite.op_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
                                                                                                      op (OfNat.ofNat n) = OfNat.ofNat n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem MulOpposite.op_intCast {α : Type u_1} [IntCast α] (n : ℤ) :
                                                                                                      op ↑n = ↑n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem AddOpposite.op_intCast {α : Type u_1} [IntCast α] (n : ℤ) :
                                                                                                      op ↑n = ↑n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem MulOpposite.unop_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
                                                                                                      unop ↑n = ↑n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem AddOpposite.unop_natCast {α : Type u_1} [NatCast α] (n : ℕ) :
                                                                                                      unop ↑n = ↑n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem MulOpposite.unop_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
                                                                                                      unop (OfNat.ofNat n) = OfNat.ofNat n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem AddOpposite.unop_ofNat {α : Type u_1} [NatCast α] (n : ℕ) [n.AtLeastTwo] :
                                                                                                      unop (OfNat.ofNat n) = OfNat.ofNat n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem MulOpposite.unop_intCast {α : Type u_1} [IntCast α] (n : ℤ) :
                                                                                                      unop ↑n = ↑n
                                                                                                      source
                                                                                                      @[simp]
                                                                                                      theorem AddOpposite.unop_intCast {α : Type u_1} [IntCast α] (n : ℤ) :
                                                                                                      unop ↑n = ↑n
                                                                                                      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
                                                                                                                            source
                                                                                                                            instance AddOpposite.instAddCommMonoidWithOne {α : Type u_1} [AddCommMonoidWithOne α] :
                                                                                                                            AddCommMonoidWithOne αᵃᵒᵖ
                                                                                                                            Equations
                                                                                                                              source
                                                                                                                              instance AddOpposite.instAddCommGroupWithOne {α : Type u_1} [AddCommGroupWithOne α] :
                                                                                                                              AddCommGroupWithOne αᵃᵒᵖ
                                                                                                                              Equations