Pull a subgroup back to an opposite subgroup along MulOpposite.unop
Instances For
Pull an additive subgroup back to an opposite additive subgroup along AddOpposite.unop
Equations
Instances For
@[simp]
@[simp]
theorem
Subgroup.mem_op
{G : Type u_2}
[Group G]
{x : Gᵐᵒᵖ}
{S : Subgroup G}
:
x ∈ S.op ↔ MulOpposite.unop x ∈ S
@[simp]
theorem
AddSubgroup.mem_op
{G : Type u_2}
[AddGroup G]
{x : Gᵃᵒᵖ}
{S : AddSubgroup G}
:
x ∈ S.op ↔ AddOpposite.unop x ∈ S
@[simp]
theorem
AddSubgroup.op_toAddSubmonoid
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup G)
:
H.op.toAddSubmonoid = H.op
Pull an opposite subgroup back to a subgroup along MulOpposite.op
Instances For
Pull an opposite additive subgroup back to an additive subgroup along AddOpposite.op
Equations
Instances For
@[simp]
@[simp]
theorem
Subgroup.mem_unop
{G : Type u_2}
[Group G]
{x : G}
{S : Subgroup Gᵐᵒᵖ}
:
x ∈ S.unop ↔ MulOpposite.op x ∈ S
@[simp]
theorem
AddSubgroup.mem_unop
{G : Type u_2}
[AddGroup G]
{x : G}
{S : AddSubgroup Gᵃᵒᵖ}
:
x ∈ S.unop ↔ AddOpposite.op x ∈ S
@[simp]
theorem
AddSubgroup.unop_toAddSubmonoid
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup Gᵃᵒᵖ)
:
H.unop.toAddSubmonoid = H.unop
@[simp]
@[simp]
Lattice results #
theorem
AddSubgroup.op_le_iff
{G : Type u_2}
[AddGroup G]
{S₁ : AddSubgroup G}
{S₂ : AddSubgroup Gᵃᵒᵖ}
:
theorem
AddSubgroup.le_op_iff
{G : Type u_2}
[AddGroup G]
{S₁ : AddSubgroup Gᵃᵒᵖ}
{S₂ : AddSubgroup G}
:
@[simp]
@[simp]
@[simp]
theorem
Subgroup.opEquiv_symm_apply
{G : Type u_2}
[Group G]
(H : Subgroup Gᵐᵒᵖ)
:
(RelIso.symm Subgroup.opEquiv) H = H.unop
@[simp]
theorem
AddSubgroup.opEquiv_symm_apply
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup Gᵃᵒᵖ)
:
(RelIso.symm AddSubgroup.opEquiv) H = H.unop
@[simp]
theorem
AddSubgroup.opEquiv_apply
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup G)
:
AddSubgroup.opEquiv H = H.op
@[simp]
@[simp]
Bijection between an additive subgroup H
and its opposite.
Equations
- H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯
Instances For
@[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_symm_apply_coe
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup G)
(b : ↥H.op)
:
↑(H.equivOp.symm b) = AddOpposite.unop ↑b
@[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
@[simp]
theorem
AddSubgroup.equivOp_apply_coe
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup G)
(a : ↥H)
:
↑(H.equivOp a) = AddOpposite.op ↑a
theorem
AddSubgroup.op_normalizer
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup G)
:
H.normalizer.op = H.op.normalizer
theorem
AddSubgroup.unop_normalizer
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup Gᵃᵒᵖ)
:
H.normalizer.unop = H.unop.normalizer