Facts about ordered structures and ordered instances on subgroups #
@[simp]
theorem
abs_mem_iff
{S : Type u_1}
{G : Type u_2}
[AddGroup G]
[LinearOrder G]
:
∀ {x : SetLike S G} [inst : NegMemClass S G] {H : S} {x_1 : G}, |x_1| ∈ H ↔ x_1 ∈ H
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
theorem
Subgroup.NormalizerCondition.normal_of_coatom
{G : Type u_1}
[Group G]
(H : Subgroup G)
(hnc : NormalizerCondition G)
(hmax : IsCoatom H)
:
H.Normal
In a group that satisfies the normalizer condition, every maximal subgroup is normal
theorem
Subgroup.isCoatom_comap_of_surjective
{G : Type u_1}
[Group G]
{H : Type u_2}
[Group H]
{φ : G →* H}
(hφ : Function.Surjective ⇑φ)
{M : Subgroup H}
(hM : IsCoatom M)
:
IsCoatom (Subgroup.comap φ M)
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_6
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_8
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_3
{G : Type u_2}
{S : Type u_1}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
:
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_1
{G : Type u_2}
{S : Type u_1}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
:
ZeroMemClass S G
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_7
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_10
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_4
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
(H : S)
:
Function.Injective fun (a : ↥H) => ↑a
@[instance 75]
instance
AddSubgroupClass.toOrderedAddCommGroup
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
An additive subgroup of an AddOrderedCommGroup
is an AddOrderedCommGroup
.
Equations
- AddSubgroupClass.toOrderedAddCommGroup H = Function.Injective.orderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_2
{G : Type u_2}
{S : Type u_1}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
:
NegMemClass S G
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_9
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toOrderedAddCommGroup.proof_5
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
↑0 = ↑0
@[instance 75]
instance
SubgroupClass.toOrderedCommGroup
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[OrderedCommGroup G]
[SubgroupClass S G]
(H : S)
:
A subgroup of an OrderedCommGroup
is an OrderedCommGroup
.
Equations
- SubgroupClass.toOrderedCommGroup H = Function.Injective.orderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_12
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
(H : S)
:
@[instance 75]
instance
AddSubgroupClass.toLinearOrderedAddCommGroup
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
An additive subgroup of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.
Equations
- AddSubgroupClass.toLinearOrderedAddCommGroup H = Function.Injective.linearOrderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_11
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
(H : S)
:
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_6
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_9
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_4
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
(H : S)
:
Function.Injective fun (a : ↥H) => ↑a
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_3
{G : Type u_2}
{S : Type u_1}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
:
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_2
{G : Type u_2}
{S : Type u_1}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
:
NegMemClass S G
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_5
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
↑0 = ↑0
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_7
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_8
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_10
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
(H : S)
:
theorem
AddSubgroupClass.toLinearOrderedAddCommGroup.proof_1
{G : Type u_2}
{S : Type u_1}
[SetLike S G]
[LinearOrderedAddCommGroup G]
[AddSubgroupClass S G]
:
ZeroMemClass S G
@[instance 75]
instance
SubgroupClass.toLinearOrderedCommGroup
{G : Type u_1}
{S : Type u_2}
[SetLike S G]
[LinearOrderedCommGroup G]
[SubgroupClass S G]
(H : S)
:
A subgroup of a LinearOrderedCommGroup
is a LinearOrderedCommGroup
.
Equations
- SubgroupClass.toLinearOrderedCommGroup H = Function.Injective.linearOrderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddSubgroup.toOrderedAddCommGroup.proof_6
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toOrderedAddCommGroup.proof_5
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
instance
AddSubgroup.toOrderedAddCommGroup
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
An AddSubgroup
of an AddOrderedCommGroup
is an AddOrderedCommGroup
.
Equations
- H.toOrderedAddCommGroup = Function.Injective.orderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddSubgroup.toOrderedAddCommGroup.proof_3
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toOrderedAddCommGroup.proof_1
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
Function.Injective fun (a : ↥H) => ↑a
theorem
AddSubgroup.toOrderedAddCommGroup.proof_2
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
↑0 = ↑0
theorem
AddSubgroup.toOrderedAddCommGroup.proof_4
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toOrderedAddCommGroup.proof_7
{G : Type u_1}
[OrderedAddCommGroup G]
(H : AddSubgroup G)
:
A subgroup of an OrderedCommGroup
is an OrderedCommGroup
.
Equations
- H.toOrderedCommGroup = Function.Injective.orderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_8
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_2
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
↑0 = ↑0
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_5
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_1
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
Function.Injective fun (a : ↥H) => ↑a
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_7
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_9
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
instance
AddSubgroup.toLinearOrderedAddCommGroup
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
An AddSubgroup
of a LinearOrderedAddCommGroup
is a
LinearOrderedAddCommGroup
.
Equations
- H.toLinearOrderedAddCommGroup = Function.Injective.linearOrderedAddCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_3
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_4
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
theorem
AddSubgroup.toLinearOrderedAddCommGroup.proof_6
{G : Type u_1}
[LinearOrderedAddCommGroup G]
(H : AddSubgroup G)
:
instance
Subgroup.toLinearOrderedCommGroup
{G : Type u_1}
[LinearOrderedCommGroup G]
(H : Subgroup G)
:
A subgroup of a LinearOrderedCommGroup
is a LinearOrderedCommGroup
.
Equations
- H.toLinearOrderedCommGroup = Function.Injective.linearOrderedCommGroup (fun (a : ↥H) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯