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
Lattice results #
theorem
AddSubgroup.unop_iSup
{ι : Sort u_1}
{G : Type u_2}
[AddGroup G]
(S : ι → AddSubgroup Gᵃᵒᵖ)
:
theorem
AddSubgroup.unop_iInf
{ι : Sort u_1}
{G : Type u_2}
[AddGroup G]
(S : ι → AddSubgroup Gᵃᵒᵖ)
:
instance
AddSubgroup.instCountableSubtypeAddOppositeMemOp
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup G)
[Countable ↥H]
:
@[simp]
@[simp]
Alias of the reverse direction of Subgroup.normal_op
.
Alias of the forward direction of Subgroup.normal_op
.
@[simp]
instance
AddSubgroup.unop.instNormal
{G : Type u_2}
[AddGroup G]
{H : AddSubgroup Gᵃᵒᵖ}
[H.Normal]
: