Subgroups #
This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled
form (unbundled subgroups are in Deprecated/Subgroups.lean
).
Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
Main definitions #
Notation used here:
G N
areGroup
sA
is anAddGroup
H K
areSubgroup
s ofG
orAddSubgroup
s ofA
x
is an element of typeG
or typeA
f g : N →* G
are group homomorphismss k
are sets of elements of typeG
Definitions in the file:
Subgroup G
: the type of subgroups of a groupG
AddSubgroup A
: the type of subgroups of an additive groupA
Subgroup.subtype
: the natural group homomorphism from a subgroup of groupG
toG
Implementation notes #
Subgroup inclusion is denoted ≤
rather than ⊆
, although ∈
is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
SubgroupClass S G
states S
is a type of subsets s ⊆ G
that are subgroups of G
.
Instances
AddSubgroupClass S G
states S
is a type of subsets s ⊆ G
that are
additive subgroups of G
.
Instances
A subgroup of a group inherits an inverse.
Equations
An additive subgroup of an AddGroup
inherits an inverse.
Equations
A subgroup of a group inherits a division
Equations
An additive subgroup of an AddGroup
inherits a subtraction.
Equations
An additive subgroup of an AddGroup
inherits an integer scaling.
Equations
A subgroup of a group inherits an integer power.
Equations
A subgroup of a group inherits a group structure.
Equations
An additive subgroup of an AddGroup
inherits an AddGroup
structure.
Equations
A subgroup of a CommGroup
is a CommGroup
.
Equations
An additive subgroup of an AddCommGroup
is an AddCommGroup
.
Equations
The natural group hom from a subgroup of group G
to G
.
Equations
Instances For
The natural group hom from an additive subgroup of AddGroup
G
to G
.
Equations
Instances For
Alias of SubgroupClass.coe_subtype
.
Alias of AddSubgroupClass.coe_subtype
.
The inclusion homomorphism from a subgroup H
contained in K
to K
.
Equations
Instances For
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
Instances For
A subgroup of a group G
is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
G
is closed under inverses
Instances For
An additive subgroup of an additive group G
is a subset containing 0, closed
under addition and additive inverse.
G
is closed under negation
Instances For
Equations
The actual Subgroup
obtained from an element of a SubgroupClass
Equations
Instances For
The actual AddSubgroup
obtained from an element of a
AddSubgroupClass
Equations
Instances For
Alias of Subgroup.toSubmonoid_inj
.
Copy of an additive subgroup with a new carrier
equal to the old one.
Useful to fix definitional equalities
Equations
Instances For
Two AddSubgroup
s are equal if they have the same elements.
An AddSubgroup
contains the group's 0.
An AddSubgroup
is closed under addition.
An AddSubgroup
is closed under inverse.
An AddSubgroup
is closed under subtraction.
An AddSubgroup
of an AddGroup
inherits an addition.
Equations
An AddSubgroup
of an AddGroup
inherits a zero.
Equations
An AddSubgroup
of an AddGroup
inherits an inverse.
Equations
An AddSubgroup
of an AddGroup
inherits a subtraction.
Equations
An AddSubgroup
of an AddGroup
inherits a natural scaling.
Equations
An AddSubgroup
of an AddGroup
inherits an integer scaling.
Equations
An AddSubgroup
of an AddGroup
inherits an AddGroup
structure.
Equations
An AddSubgroup
of an AddCommGroup
is an AddCommGroup
.
Equations
Alias of Subgroup.coe_subtype
.
Alias of AddSubgroup.coe_subtype
.
The inclusion homomorphism from an additive subgroup H
contained in K
to K
.
Equations
Instances For
Alias of IsMulCommutative
.
A Prop stating that the multiplication is commutative.
Equations
Instances For
Alias of IsAddCommutative
.
A Prop stating that the addition is commutative.
Equations
Instances For
A subgroup of a commutative group is commutative.
A subgroup of a commutative group is commutative.
Alias of Subgroup.commGroup_isMulCommutative
.
A subgroup of a commutative group is commutative.
Alias of Subgroup.commGroup_isMulCommutative
.
A subgroup of a commutative group is commutative.