Documentation

Mathlib.Algebra.Group.Subgroup.MulOpposite

Mul-opposite subgroups #

Tags #

subgroup, subgroups

def Subgroup.op {G : Type u_2} [Group G] (H : Subgroup G) :

Pull a subgroup back to an opposite subgroup along MulOpposite.unop

Equations
    Instances For

      Pull an additive subgroup back to an opposite additive subgroup along AddOpposite.unop

      Equations
        Instances For
          @[simp]
          theorem AddSubgroup.coe_op {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
          @[simp]
          theorem Subgroup.coe_op {G : Type u_2} [Group G] (H : Subgroup G) :
          @[simp]
          theorem Subgroup.mem_op {G : Type u_2} [Group G] {x : Gᵐᵒᵖ} {S : Subgroup G} :
          @[simp]
          theorem AddSubgroup.mem_op {G : Type u_2} [AddGroup G] {x : Gᵃᵒᵖ} {S : AddSubgroup G} :
          @[simp]
          theorem Subgroup.op_toSubmonoid {G : Type u_2} [Group G] (H : Subgroup G) :
          def Subgroup.unop {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :

          Pull an opposite subgroup back to a subgroup along MulOpposite.op

          Equations
            Instances For

              Pull an opposite additive subgroup back to an additive subgroup along AddOpposite.op

              Equations
                Instances For
                  @[simp]
                  theorem Subgroup.coe_unop {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
                  @[simp]
                  @[simp]
                  theorem Subgroup.mem_unop {G : Type u_2} [Group G] {x : G} {S : Subgroup Gᵐᵒᵖ} :
                  @[simp]
                  theorem AddSubgroup.mem_unop {G : Type u_2} [AddGroup G] {x : G} {S : AddSubgroup Gᵃᵒᵖ} :
                  @[simp]
                  theorem Subgroup.unop_op {G : Type u_2} [Group G] (S : Subgroup G) :
                  S.op.unop = S
                  @[simp]
                  theorem AddSubgroup.unop_op {G : Type u_2} [AddGroup G] (S : AddSubgroup G) :
                  S.op.unop = S
                  @[simp]
                  theorem Subgroup.op_unop {G : Type u_2} [Group G] (S : Subgroup Gᵐᵒᵖ) :
                  S.unop.op = S
                  @[simp]
                  theorem AddSubgroup.op_unop {G : Type u_2} [AddGroup G] (S : AddSubgroup Gᵃᵒᵖ) :
                  S.unop.op = S

                  Lattice results #

                  theorem Subgroup.op_le_iff {G : Type u_2} [Group G] {S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ} :
                  S₁.op S₂ S₁ S₂.unop
                  theorem AddSubgroup.op_le_iff {G : Type u_2} [AddGroup G] {S₁ : AddSubgroup G} {S₂ : AddSubgroup Gᵃᵒᵖ} :
                  S₁.op S₂ S₁ S₂.unop
                  theorem Subgroup.le_op_iff {G : Type u_2} [Group G] {S₁ : Subgroup Gᵐᵒᵖ} {S₂ : Subgroup G} :
                  S₁ S₂.op S₁.unop S₂
                  theorem AddSubgroup.le_op_iff {G : Type u_2} [AddGroup G] {S₁ : AddSubgroup Gᵃᵒᵖ} {S₂ : AddSubgroup G} :
                  S₁ S₂.op S₁.unop S₂
                  @[simp]
                  theorem Subgroup.op_le_op_iff {G : Type u_2} [Group G] {S₁ S₂ : Subgroup G} :
                  S₁.op S₂.op S₁ S₂
                  @[simp]
                  theorem AddSubgroup.op_le_op_iff {G : Type u_2} [AddGroup G] {S₁ S₂ : AddSubgroup G} :
                  S₁.op S₂.op S₁ S₂
                  @[simp]
                  theorem Subgroup.unop_le_unop_iff {G : Type u_2} [Group G] {S₁ S₂ : Subgroup Gᵐᵒᵖ} :
                  S₁.unop S₂.unop S₁ S₂
                  @[simp]
                  theorem AddSubgroup.unop_le_unop_iff {G : Type u_2} [AddGroup G] {S₁ S₂ : AddSubgroup Gᵃᵒᵖ} :
                  S₁.unop S₂.unop S₁ S₂

                  A subgroup H of G determines a subgroup H.op of the opposite group Gᵐᵒᵖ.

                  Equations
                    Instances For

                      An additive subgroup H of G determines an additive subgroup H.op of the opposite additive group Gᵃᵒᵖ.

                      Equations
                        Instances For
                          @[simp]
                          theorem AddSubgroup.opEquiv_apply {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
                          @[simp]
                          theorem Subgroup.opEquiv_apply {G : Type u_2} [Group G] (H : Subgroup G) :
                          @[simp]
                          theorem Subgroup.op_inj {G : Type u_2} [Group G] {S T : Subgroup G} :
                          S.op = T.op S = T
                          @[simp]
                          theorem AddSubgroup.op_inj {G : Type u_2} [AddGroup G] {S T : AddSubgroup G} :
                          S.op = T.op S = T
                          @[simp]
                          theorem Subgroup.unop_inj {G : Type u_2} [Group G] {S T : Subgroup Gᵐᵒᵖ} :
                          S.unop = T.unop S = T
                          @[simp]
                          theorem AddSubgroup.unop_inj {G : Type u_2} [AddGroup G] {S T : AddSubgroup Gᵃᵒᵖ} :
                          S.unop = T.unop S = T
                          def Subgroup.equivOp {G : Type u_2} [Group G] (H : Subgroup G) :
                          H H.op

                          Bijection between a subgroup H and its opposite.

                          Equations
                            Instances For
                              def AddSubgroup.equivOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
                              H H.op

                              Bijection between an additive subgroup H and its opposite.

                              Equations
                                Instances For
                                  @[simp]
                                  theorem Subgroup.equivOp_symm_apply_coe {G : Type u_2} [Group G] (H : Subgroup G) (b : H.op) :
                                  @[simp]
                                  theorem Subgroup.equivOp_apply_coe {G : Type u_2} [Group G] (H : Subgroup G) (a : H) :
                                  (H.equivOp a) = MulOpposite.op a
                                  @[simp]
                                  theorem AddSubgroup.equivOp_apply_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (a : H) :
                                  (H.equivOp a) = AddOpposite.op a
                                  @[simp]
                                  theorem AddSubgroup.equivOp_symm_apply_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (b : H.op) :