Documentation

Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Mul-opposite subgroups #

This file contains a somewhat arbitrary assortment of results on the opposite subgroup H.op that rely on further theory to define. As such it is a somewhat arbitrary assortment of results, which might be organized and split up further.

Tags #

subgroup, subgroups

source
instance Subgroup.instSMul {G : Type u_2} [Group G] (H : Subgroup G) :
SMul (↥H.op) G
Equations
  • H.instSMul = H.op.smul
source
instance AddSubgroup.instVAdd {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
VAdd (↥H.op) G
Equations
  • H.instVAdd = H.op.vadd

Lattice results #

source
@[simp]
theorem Subgroup.op_bot {G : Type u_2} [Group G] :
⊥.op = ⊥
source
@[simp]
theorem AddSubgroup.op_bot {G : Type u_2} [AddGroup G] :
⊥.op = ⊥
source
@[simp]
theorem Subgroup.op_eq_bot {G : Type u_2} [Group G] {S : Subgroup G} :
S.op = ⊥ ↔ S = ⊥
source
@[simp]
theorem AddSubgroup.op_eq_bot {G : Type u_2} [AddGroup G] {S : AddSubgroup G} :
S.op = ⊥ ↔ S = ⊥
source
@[simp]
theorem Subgroup.unop_bot {G : Type u_2} [Group G] :
⊥.unop = ⊥
source
@[simp]
theorem AddSubgroup.unop_bot {G : Type u_2} [AddGroup G] :
⊥.unop = ⊥
source
@[simp]
theorem Subgroup.unop_eq_bot {G : Type u_2} [Group G] {S : Subgroup Gᵐᵒᵖ} :
S.unop = ⊥ ↔ S = ⊥
source
@[simp]
theorem AddSubgroup.unop_eq_bot {G : Type u_2} [AddGroup G] {S : AddSubgroup Gᵃᵒᵖ} :
S.unop = ⊥ ↔ S = ⊥
source
@[simp]
theorem Subgroup.op_top {G : Type u_2} [Group G] :
⊤.op = ⊤
source
@[simp]
theorem AddSubgroup.op_top {G : Type u_2} [AddGroup G] :
⊤.op = ⊤
source
@[simp]
theorem Subgroup.op_eq_top {G : Type u_2} [Group G] {S : Subgroup G} :
S.op = ⊤ ↔ S = ⊤
source
@[simp]
theorem AddSubgroup.op_eq_top {G : Type u_2} [AddGroup G] {S : AddSubgroup G} :
S.op = ⊤ ↔ S = ⊤
source
@[simp]
theorem Subgroup.unop_top {G : Type u_2} [Group G] :
⊤.unop = ⊤
source
@[simp]
theorem AddSubgroup.unop_top {G : Type u_2} [AddGroup G] :
⊤.unop = ⊤
source
@[simp]
theorem Subgroup.unop_eq_top {G : Type u_2} [Group G] {S : Subgroup Gᵐᵒᵖ} :
S.unop = ⊤ ↔ S = ⊤
source
@[simp]
theorem AddSubgroup.unop_eq_top {G : Type u_2} [AddGroup G] {S : AddSubgroup Gᵃᵒᵖ} :
S.unop = ⊤ ↔ S = ⊤
source
theorem Subgroup.op_sup {G : Type u_2} [Group G] (S₁ : Subgroup G) (S₂ : Subgroup G) :
(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
source
theorem AddSubgroup.op_sup {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup G) (S₂ : AddSubgroup G) :
(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
source
theorem Subgroup.unop_sup {G : Type u_2} [Group G] (S₁ : Subgroup Gᵐᵒᵖ) (S₂ : Subgroup Gᵐᵒᵖ) :
(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
source
theorem AddSubgroup.unop_sup {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup Gᵃᵒᵖ) (S₂ : AddSubgroup Gᵃᵒᵖ) :
(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
source
theorem Subgroup.op_inf {G : Type u_2} [Group G] (S₁ : Subgroup G) (S₂ : Subgroup G) :
(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
source
theorem AddSubgroup.op_inf {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup G) (S₂ : AddSubgroup G) :
(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
source
theorem Subgroup.unop_inf {G : Type u_2} [Group G] (S₁ : Subgroup Gᵐᵒᵖ) (S₂ : Subgroup Gᵐᵒᵖ) :
(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
source
theorem AddSubgroup.unop_inf {G : Type u_2} [AddGroup G] (S₁ : AddSubgroup Gᵃᵒᵖ) (S₂ : AddSubgroup Gᵃᵒᵖ) :
(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
source
theorem Subgroup.op_sSup {G : Type u_2} [Group G] (S : Set (Subgroup G)) :
(sSup S).op = sSup (Subgroup.unop ⁻¹' S)
source
theorem AddSubgroup.op_sSup {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup G)) :
(sSup S).op = sSup (AddSubgroup.unop ⁻¹' S)
source
theorem Subgroup.unop_sSup {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) :
(sSup S).unop = sSup (Subgroup.op ⁻¹' S)
source
theorem AddSubgroup.unop_sSup {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)) :
(sSup S).unop = sSup (AddSubgroup.op ⁻¹' S)
source
theorem Subgroup.op_sInf {G : Type u_2} [Group G] (S : Set (Subgroup G)) :
(sInf S).op = sInf (Subgroup.unop ⁻¹' S)
source
theorem AddSubgroup.op_sInf {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup G)) :
(sInf S).op = sInf (AddSubgroup.unop ⁻¹' S)
source
theorem Subgroup.unop_sInf {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) :
(sInf S).unop = sInf (Subgroup.op ⁻¹' S)
source
theorem AddSubgroup.unop_sInf {G : Type u_2} [AddGroup G] (S : Set (AddSubgroup Gᵃᵒᵖ)) :
(sInf S).unop = sInf (AddSubgroup.op ⁻¹' S)
source
theorem Subgroup.op_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) :
(iSup S).op = ⨆ (i : ι), (S i).op
source
theorem AddSubgroup.op_iSup {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup G) :
(iSup S).op = ⨆ (i : ι), (S i).op
source
theorem Subgroup.unop_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) :
(iSup S).unop = ⨆ (i : ι), (S i).unop
source
theorem AddSubgroup.unop_iSup {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ) :
(iSup S).unop = ⨆ (i : ι), (S i).unop
source
theorem Subgroup.op_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) :
(iInf S).op = ⨅ (i : ι), (S i).op
source
theorem AddSubgroup.op_iInf {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup G) :
(iInf S).op = ⨅ (i : ι), (S i).op
source
theorem Subgroup.unop_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) :
(iInf S).unop = ⨅ (i : ι), (S i).unop
source
theorem AddSubgroup.unop_iInf {ι : Sort u_1} {G : Type u_2} [AddGroup G] (S : ι → AddSubgroup Gᵃᵒᵖ) :
(iInf S).unop = ⨅ (i : ι), (S i).unop
source
theorem Subgroup.op_closure {G : Type u_2} [Group G] (s : Set G) :
(Subgroup.closure s).op = Subgroup.closure (MulOpposite.unop ⁻¹' s)
source
theorem AddSubgroup.op_closure {G : Type u_2} [AddGroup G] (s : Set G) :
(AddSubgroup.closure s).op = AddSubgroup.closure (AddOpposite.unop ⁻¹' s)
source
theorem Subgroup.unop_closure {G : Type u_2} [Group G] (s : Set Gᵐᵒᵖ) :
(Subgroup.closure s).unop = Subgroup.closure (MulOpposite.op ⁻¹' s)
source
theorem AddSubgroup.unop_closure {G : Type u_2} [AddGroup G] (s : Set Gᵃᵒᵖ) :
(AddSubgroup.closure s).unop = AddSubgroup.closure (AddOpposite.op ⁻¹' s)
source
instance Subgroup.instEncodableSubtypeMulOppositeMemOp {G : Type u_2} [Group G] (H : Subgroup G) [Encodable ↥H] :
Encodable ↥H.op
Equations
source
instance AddSubgroup.instEncodableSubtypeAddOppositeMemOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Encodable ↥H] :
Encodable ↥H.op
Equations
source
instance Subgroup.instCountableSubtypeMulOppositeMemOp {G : Type u_2} [Group G] (H : Subgroup G) [Countable ↥H] :
Countable ↥H.op
Equations
  • ⋯ = ⋯
source
instance AddSubgroup.instCountableSubtypeAddOppositeMemOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Countable ↥H] :
Countable ↥H.op
Equations
  • ⋯ = ⋯
source
theorem Subgroup.smul_opposite_mul {G : Type u_2} [Group G] {H : Subgroup G} (x : G) (g : G) (h : ↥H.op) :
h • (g * x) = g * h • x
source
theorem AddSubgroup.vadd_opposite_add {G : Type u_2} [AddGroup G] {H : AddSubgroup G} (x : G) (g : G) (h : ↥H.op) :
h +ᵥ (g + x) = g + (h +ᵥ x)
source
@[simp]
theorem Subgroup.normal_op {G : Type u_2} [Group G] {H : Subgroup G} :
H.op.Normal ↔ H.Normal
source
@[simp]
theorem AddSubgroup.normal_op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} :
H.op.Normal ↔ H.Normal
source
theorem Subgroup.Normal.op {G : Type u_2} [Group G] {H : Subgroup G} :
H.Normal → H.op.Normal

Alias of the reverse direction of Subgroup.normal_op.

source
theorem Subgroup.Normal.of_op {G : Type u_2} [Group G] {H : Subgroup G} :
H.op.Normal → H.Normal

Alias of the forward direction of Subgroup.normal_op.

source
theorem AddSubgroup.Normal.of_op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} :
H.op.Normal → H.Normal
source
theorem AddSubgroup.Normal.op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} :
H.Normal → H.op.Normal
source
instance Subgroup.op.instNormal {G : Type u_2} [Group G] {H : Subgroup G} [H.Normal] :
H.op.Normal
Equations
  • ⋯ = ⋯
source
instance AddSubgroup.op.instNormal {G : Type u_2} [AddGroup G] {H : AddSubgroup G} [H.Normal] :
H.op.Normal
Equations
  • ⋯ = ⋯
source
@[simp]
theorem Subgroup.normal_unop {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} :
H.unop.Normal ↔ H.Normal
source
@[simp]
theorem AddSubgroup.normal_unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} :
H.unop.Normal ↔ H.Normal
source
theorem Subgroup.Normal.unop {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} :
H.Normal → H.unop.Normal

Alias of the reverse direction of Subgroup.normal_unop.

source
theorem Subgroup.Normal.of_unop {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} :
H.unop.Normal → H.Normal

Alias of the forward direction of Subgroup.normal_unop.

source
theorem AddSubgroup.Normal.of_unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} :
H.unop.Normal → H.Normal
source
theorem AddSubgroup.Normal.unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} :
H.Normal → H.unop.Normal
source
instance Subgroup.unop.instNormal {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} [H.Normal] :
H.unop.Normal
Equations
  • ⋯ = ⋯
source
instance AddSubgroup.unop.instNormal {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} [H.Normal] :
H.unop.Normal
Equations
  • ⋯ = ⋯