Documentation

Mathlib.Algebra.Group.Subgroup.MulOpposite

Mul-opposite subgroups #

Tags #

subgroup, subgroups

source
theorem AddSubgroup.op.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
∀ {a b : Gᵃᵒᵖ}, a ∈ AddOpposite.unop ⁻¹' ↑H → b ∈ AddOpposite.unop ⁻¹' ↑H → AddOpposite.unop b + AddOpposite.unop a ∈ H
source
def AddSubgroup.op {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
AddSubgroup Gᵃᵒᵖ

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

Equations
  • H.op = { carrier := AddOpposite.unop ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
source
theorem AddSubgroup.op.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
∀ {x : Gᵃᵒᵖ}, AddOpposite.unop x ∈ H → -AddOpposite.unop x ∈ H
source
@[simp]
theorem Subgroup.op_coe {G : Type u_2} [Group G] (H : Subgroup G) :
↑H.op = MulOpposite.unop ⁻¹' ↑H
source
@[simp]
theorem AddSubgroup.op_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
↑H.op = AddOpposite.unop ⁻¹' ↑H
source
def Subgroup.op {G : Type u_2} [Group G] (H : Subgroup G) :
Subgroup Gᵐᵒᵖ

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

Equations
  • H.op = { carrier := MulOpposite.unop ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
source
instance AddSubgroup.instVAdd {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
VAdd (↥H.op) G
Equations
  • H.instVAdd = H.op.vadd
source
instance Subgroup.instSMul {G : Type u_2} [Group G] (H : Subgroup G) :
SMul (↥H.op) G
Equations
  • H.instSMul = H.op.smul
source
@[simp]
theorem AddSubgroup.mem_op {G : Type u_2} [AddGroup G] {x : Gᵃᵒᵖ} {S : AddSubgroup G} :
x ∈ S.op ↔ AddOpposite.unop x ∈ S
source
@[simp]
theorem Subgroup.mem_op {G : Type u_2} [Group G] {x : Gᵐᵒᵖ} {S : Subgroup G} :
x ∈ S.op ↔ MulOpposite.unop x ∈ S
source
@[simp]
theorem AddSubgroup.op_toAddSubmonoid {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
H.op.toAddSubmonoid = H.op
source
@[simp]
theorem Subgroup.op_toSubmonoid {G : Type u_2} [Group G] (H : Subgroup G) :
H.op.toSubmonoid = H.op
source
theorem AddSubgroup.unop.proof_2 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
0 ∈ H
source
theorem AddSubgroup.unop.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
∀ {a b : G}, a ∈ AddOpposite.op ⁻¹' ↑H → b ∈ AddOpposite.op ⁻¹' ↑H → { unop' := b } + { unop' := a } ∈ H
source
def AddSubgroup.unop {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
AddSubgroup G

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

Equations
  • H.unop = { carrier := AddOpposite.op ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
source
theorem AddSubgroup.unop.proof_3 {G : Type u_1} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
∀ {x : G}, AddOpposite.op x ∈ H → -AddOpposite.op x ∈ H
source
@[simp]
theorem Subgroup.unop_coe {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
↑H.unop = MulOpposite.op ⁻¹' ↑H
source
@[simp]
theorem AddSubgroup.unop_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
↑H.unop = AddOpposite.op ⁻¹' ↑H
source
def Subgroup.unop {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
Subgroup G

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

Equations
  • H.unop = { carrier := MulOpposite.op ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
source
@[simp]
theorem AddSubgroup.mem_unop {G : Type u_2} [AddGroup G] {x : G} {S : AddSubgroup Gᵃᵒᵖ} :
x ∈ S.unop ↔ AddOpposite.op x ∈ S
source
@[simp]
theorem Subgroup.mem_unop {G : Type u_2} [Group G] {x : G} {S : Subgroup Gᵐᵒᵖ} :
x ∈ S.unop ↔ MulOpposite.op x ∈ S
source
@[simp]
theorem AddSubgroup.unop_toAddSubmonoid {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
H.unop.toAddSubmonoid = H.unop
source
@[simp]
theorem Subgroup.unop_toSubmonoid {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
H.unop.toSubmonoid = H.unop
source
@[simp]
theorem AddSubgroup.unop_op {G : Type u_2} [AddGroup G] (S : AddSubgroup G) :
S.op.unop = S
source
@[simp]
theorem Subgroup.unop_op {G : Type u_2} [Group G] (S : Subgroup G) :
S.op.unop = S
source
@[simp]
theorem AddSubgroup.op_unop {G : Type u_2} [AddGroup G] (S : AddSubgroup Gᵃᵒᵖ) :
S.unop.op = S
source
@[simp]
theorem Subgroup.op_unop {G : Type u_2} [Group G] (S : Subgroup Gᵐᵒᵖ) :
S.unop.op = S

Lattice results #

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

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

Equations
  • AddSubgroup.opEquiv = { toFun := AddSubgroup.op, invFun := AddSubgroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
source
@[simp]
theorem AddSubgroup.opEquiv_apply {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
AddSubgroup.opEquiv H = H.op
source
@[simp]
theorem AddSubgroup.opEquiv_symm_apply {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
(RelIso.symm AddSubgroup.opEquiv) H = H.unop
source
@[simp]
theorem Subgroup.opEquiv_apply {G : Type u_2} [Group G] (H : Subgroup G) :
Subgroup.opEquiv H = H.op
source
@[simp]
theorem Subgroup.opEquiv_symm_apply {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
(RelIso.symm Subgroup.opEquiv) H = H.unop
source
def Subgroup.opEquiv {G : Type u_2} [Group G] :
Subgroup G ≃o Subgroup Gᵐᵒᵖ

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

Equations
  • Subgroup.opEquiv = { toFun := Subgroup.op, invFun := Subgroup.unop, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
source
theorem AddSubgroup.op_injective {G : Type u_2} [AddGroup G] :
Function.Injective AddSubgroup.op
source
theorem Subgroup.op_injective {G : Type u_2} [Group G] :
Function.Injective Subgroup.op
source
theorem AddSubgroup.unop_injective {G : Type u_2} [AddGroup G] :
Function.Injective AddSubgroup.unop
source
theorem Subgroup.unop_injective {G : Type u_2} [Group G] :
Function.Injective Subgroup.unop
source
@[simp]
theorem AddSubgroup.op_inj {G : Type u_2} [AddGroup G] {S : AddSubgroup G} {T : AddSubgroup G} :
S.op = T.op ↔ S = T
source
@[simp]
theorem Subgroup.op_inj {G : Type u_2} [Group G] {S : Subgroup G} {T : Subgroup G} :
S.op = T.op ↔ S = T
source
@[simp]
theorem AddSubgroup.unop_inj {G : Type u_2} [AddGroup G] {S : AddSubgroup Gᵃᵒᵖ} {T : AddSubgroup Gᵃᵒᵖ} :
S.unop = T.unop ↔ S = T
source
@[simp]
theorem Subgroup.unop_inj {G : Type u_2} [Group G] {S : Subgroup Gᵐᵒᵖ} {T : Subgroup Gᵐᵒᵖ} :
S.unop = T.unop ↔ S = T
source
@[simp]
theorem AddSubgroup.op_bot {G : Type u_2} [AddGroup G] :
⊥.op = ⊥
source
@[simp]
theorem Subgroup.op_bot {G : Type u_2} [Group G] :
⊥.op = ⊥
source
@[simp]
theorem AddSubgroup.op_eq_bot {G : Type u_2} [AddGroup G] {S : AddSubgroup G} :
S.op = ⊥ ↔ S = ⊥
source
@[simp]
theorem Subgroup.op_eq_bot {G : Type u_2} [Group G] {S : Subgroup G} :
S.op = ⊥ ↔ S = ⊥
source
@[simp]
theorem AddSubgroup.unop_bot {G : Type u_2} [AddGroup G] :
⊥.unop = ⊥
source
@[simp]
theorem Subgroup.unop_bot {G : Type u_2} [Group G] :
⊥.unop = ⊥
source
@[simp]
theorem AddSubgroup.unop_eq_bot {G : Type u_2} [AddGroup G] {S : AddSubgroup Gᵃᵒᵖ} :
S.unop = ⊥ ↔ S = ⊥
source
@[simp]
theorem Subgroup.unop_eq_bot {G : Type u_2} [Group G] {S : Subgroup Gᵐᵒᵖ} :
S.unop = ⊥ ↔ S = ⊥
source
@[simp]
theorem AddSubgroup.op_top {G : Type u_2} [AddGroup G] :
⊤.op = ⊤
source
@[simp]
theorem Subgroup.op_top {G : Type u_2} [Group G] :
⊤.op = ⊤
source
@[simp]
theorem AddSubgroup.op_eq_top {G : Type u_2} [AddGroup G] {S : AddSubgroup G} :
S.op = ⊤ ↔ S = ⊤
source
@[simp]
theorem Subgroup.op_eq_top {G : Type u_2} [Group G] {S : Subgroup G} :
S.op = ⊤ ↔ S = ⊤
source
@[simp]
theorem AddSubgroup.unop_top {G : Type u_2} [AddGroup G] :
⊤.unop = ⊤
source
@[simp]
theorem Subgroup.unop_top {G : Type u_2} [Group G] :
⊤.unop = ⊤
source
@[simp]
theorem AddSubgroup.unop_eq_top {G : Type u_2} [AddGroup G] {S : AddSubgroup Gᵃᵒᵖ} :
S.unop = ⊤ ↔ S = ⊤
source
@[simp]
theorem Subgroup.unop_eq_top {G : Type u_2} [Group G] {S : Subgroup Gᵐᵒᵖ} :
S.unop = ⊤ ↔ S = ⊤
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.op_sup {G : Type u_2} [Group G] (S₁ : Subgroup G) (S₂ : Subgroup G) :
(S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op
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.unop_sup {G : Type u_2} [Group G] (S₁ : Subgroup Gᵐᵒᵖ) (S₂ : Subgroup Gᵐᵒᵖ) :
(S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
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.op_inf {G : Type u_2} [Group G] (S₁ : Subgroup G) (S₂ : Subgroup G) :
(S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op
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.unop_inf {G : Type u_2} [Group G] (S₁ : Subgroup Gᵐᵒᵖ) (S₂ : Subgroup Gᵐᵒᵖ) :
(S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
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.op_sSup {G : Type u_2} [Group G] (S : Set (Subgroup G)) :
(sSup S).op = sSup (Subgroup.unop ⁻¹' 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.unop_sSup {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) :
(sSup S).unop = sSup (Subgroup.op ⁻¹' 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.op_sInf {G : Type u_2} [Group G] (S : Set (Subgroup G)) :
(sInf S).op = sInf (Subgroup.unop ⁻¹' 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.unop_sInf {G : Type u_2} [Group G] (S : Set (Subgroup Gᵐᵒᵖ)) :
(sInf S).unop = sInf (Subgroup.op ⁻¹' S)
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.op_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) :
(iSup S).op = ⨆ (i : ι), (S i).op
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.unop_iSup {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) :
(iSup S).unop = ⨆ (i : ι), (S i).unop
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.op_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup G) :
(iInf S).op = ⨅ (i : ι), (S i).op
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.unop_iInf {ι : Sort u_1} {G : Type u_2} [Group G] (S : ι → Subgroup Gᵐᵒᵖ) :
(iInf S).unop = ⨅ (i : ι), (S i).unop
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.op_closure {G : Type u_2} [Group G] (s : Set G) :
(Subgroup.closure s).op = Subgroup.closure (MulOpposite.unop ⁻¹' 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
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.equivOp.proof_1 {G : Type u_1} [AddGroup G] (H : AddSubgroup G) :
∀ (x : G), x ∈ H ↔ x ∈ H
source
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
  • H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯
source
@[simp]
theorem AddSubgroup.equivOp_symm_apply_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (b : ↥H.op) :
↑(H.equivOp.symm b) = AddOpposite.unop ↑b
source
@[simp]
theorem Subgroup.equivOp_symm_apply_coe {G : Type u_2} [Group G] (H : Subgroup G) (b : ↥H.op) :
↑(H.equivOp.symm b) = MulOpposite.unop ↑b
source
@[simp]
theorem Subgroup.equivOp_apply_coe {G : Type u_2} [Group G] (H : Subgroup G) (a : ↥H) :
↑(H.equivOp a) = MulOpposite.op ↑a
source
@[simp]
theorem AddSubgroup.equivOp_apply_coe {G : Type u_2} [AddGroup G] (H : AddSubgroup G) (a : ↥H) :
↑(H.equivOp a) = AddOpposite.op ↑a
source
def Subgroup.equivOp {G : Type u_2} [Group G] (H : Subgroup G) :
↥H ≃ ↥H.op

Bijection between a subgroup H and its opposite.

Equations
  • H.equivOp = MulOpposite.opEquiv.subtypeEquiv ⋯
source
instance AddSubgroup.instEncodableSubtypeAddOppositeMemOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Encodable ↥H] :
Encodable ↥H.op
Equations
source
instance Subgroup.instEncodableSubtypeMulOppositeMemOp {G : Type u_2} [Group G] (H : Subgroup G) [Encodable ↥H] :
Encodable ↥H.op
Equations
source
instance AddSubgroup.instCountableSubtypeAddOppositeMemOp {G : Type u_2} [AddGroup G] (H : AddSubgroup G) [Countable ↥H] :
Countable ↥H.op
Equations
  • ⋯ = ⋯
source
instance Subgroup.instCountableSubtypeMulOppositeMemOp {G : Type u_2} [Group G] (H : Subgroup G) [Countable ↥H] :
Countable ↥H.op
Equations
  • ⋯ = ⋯
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
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.op_normalizer {G : Type u_2} [AddGroup G] (H : AddSubgroup G) :
H.normalizer.op = H.op.normalizer
source
theorem Subgroup.op_normalizer {G : Type u_2} [Group G] (H : Subgroup G) :
H.normalizer.op = H.op.normalizer
source
theorem AddSubgroup.unop_normalizer {G : Type u_2} [AddGroup G] (H : AddSubgroup Gᵃᵒᵖ) :
H.normalizer.unop = H.unop.normalizer
source
theorem Subgroup.unop_normalizer {G : Type u_2} [Group G] (H : Subgroup Gᵐᵒᵖ) :
H.normalizer.unop = H.unop.normalizer
source
@[simp]
theorem AddSubgroup.normal_op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} :
H.op.Normal ↔ H.Normal
source
@[simp]
theorem Subgroup.normal_op {G : Type u_2} [Group G] {H : Subgroup 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.op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} :
H.Normal → H.op.Normal
source
theorem AddSubgroup.Normal.of_op {G : Type u_2} [AddGroup G] {H : AddSubgroup G} :
H.op.Normal → H.Normal
source
instance AddSubgroup.op.instNormal {G : Type u_2} [AddGroup G] {H : AddSubgroup G} [H.Normal] :
H.op.Normal
Equations
  • ⋯ = ⋯
source
instance Subgroup.op.instNormal {G : Type u_2} [Group G] {H : Subgroup G} [H.Normal] :
H.op.Normal
Equations
  • ⋯ = ⋯
source
@[simp]
theorem AddSubgroup.normal_unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} :
H.unop.Normal ↔ H.Normal
source
@[simp]
theorem Subgroup.normal_unop {G : Type u_2} [Group G] {H : Subgroup 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.unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} :
H.Normal → H.unop.Normal
source
theorem AddSubgroup.Normal.of_unop {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} :
H.unop.Normal → H.Normal
source
instance AddSubgroup.unop.instNormal {G : Type u_2} [AddGroup G] {H : AddSubgroup Gᵃᵒᵖ} [H.Normal] :
H.unop.Normal
Equations
  • ⋯ = ⋯
source
instance Subgroup.unop.instNormal {G : Type u_2} [Group G] {H : Subgroup Gᵐᵒᵖ} [H.Normal] :
H.unop.Normal
Equations
  • ⋯ = ⋯