Subgroups #
This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled
form (unbundled subgroups are in deprecated/subgroups.lean).
We prove subgroups of a group form a complete lattice, and results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.
There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.
Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
Main definitions #
Notation used here:
-
G Naregroups -
Ais anadd_group -
H Karesubgroups ofGoradd_subgroups ofA -
xis an element of typeGor typeA -
f g : N →* Gare group homomorphisms -
s kare sets of elements of typeG
Definitions in the file:
-
subgroup G: the type of subgroups of a groupG -
add_subgroup A: the type of subgroups of an additive groupA -
complete_lattice (subgroup G): the subgroups ofGform a complete lattice -
subgroup.closure k: the minimal subgroup that includes the setk -
subgroup.subtype: the natural group homomorphism from a subgroup of groupGtoG -
subgroup.gi:closureforms a Galois insertion with the coercion to set -
subgroup.comap H f: the preimage of a subgroupHalong the group homomorphismfis also a subgroup -
subgroup.map f H: the image of a subgroupHalong the group homomorphismfis also a subgroup -
subgroup.prod H K: the product of subgroupsH,Kof groupsG,Nrespectively,H × Kis a subgroup ofG × N -
monoid_hom.range f: the range of the group homomorphismfis a subgroup -
monoid_hom.ker f: the kernel of a group homomorphismfis the subgroup of elementsx : Gsuch thatf x = 1 -
monoid_hom.eq_locus f g: given group homomorphismsf,g, the elements ofGsuch thatf x = g xform a subgroup ofG -
is_simple_group G: a class indicating that a group has exactly two normal subgroups
Implementation notes #
Subgroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
@[class]
inv_mem_class S G states S is a type of subsets s ⊆ G closed under inverses.
Instances of this typeclass
Instances of other typeclasses for inv_mem_class
- inv_mem_class.has_sizeof_inst
@[class]
neg_mem_class S G states S is a type of subsets s ⊆ G closed under negation.
Instances of this typeclass
Instances of other typeclasses for neg_mem_class
- neg_mem_class.has_sizeof_inst
@[class]
- to_submonoid_class : submonoid_class S G
- inv_mem : ∀ {s : S} {x : G}, x ∈ s → x⁻¹ ∈ s
subgroup_class S G states S is a type of subsets s ⊆ G that are subgroups of G.
Instances of this typeclass
Instances of other typeclasses for subgroup_class
- subgroup_class.has_sizeof_inst
@[class]
- to_add_submonoid_class : add_submonoid_class S G
- neg_mem : ∀ {s : S} {x : G}, x ∈ s → -x ∈ s
add_subgroup_class S G states S is a type of subsets s ⊆ G that are
additive subgroups of G.
Instances of this typeclass
Instances of other typeclasses for add_subgroup_class
- add_subgroup_class.has_sizeof_inst
@[protected, instance]
def
add_subgroup_class.to_neg_mem_class
(M : Type u_3)
(S : Type u_4)
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M] :
neg_mem_class S M
Equations
- add_subgroup_class.to_neg_mem_class M S = {neg_mem := _}
@[protected, instance]
def
subgroup_class.to_inv_mem_class
(M : Type u_3)
(S : Type u_4)
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M] :
inv_mem_class S M
Equations
- subgroup_class.to_inv_mem_class M S = {inv_mem := _}
theorem
div_mem
{M : Type u_3}
{S : Type u_4}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S}
{x y : M}
(hx : x ∈ H)
(hy : y ∈ H) :
A subgroup is closed under division.
theorem
sub_mem
{M : Type u_3}
{S : Type u_4}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S}
{x y : M}
(hx : x ∈ H)
(hy : y ∈ H) :
An additive subgroup is closed under subtraction.
theorem
zpow_mem
{M : Type u_3}
{S : Type u_4}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{K : S}
{x : M}
(hx : x ∈ K)
(n : ℤ) :
theorem
zsmul_mem
{M : Type u_3}
{S : Type u_4}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{K : S}
{x : M}
(hx : x ∈ K)
(n : ℤ) :
@[simp]
theorem
neg_mem_iff
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G]
{x : G} :
@[simp]
theorem
inv_mem_iff
{G : Type u_1}
[group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : subgroup_class S G]
{x : G} :
theorem
sub_mem_comm_iff
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G]
{a b : G} :
theorem
div_mem_comm_iff
{G : Type u_1}
[group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : subgroup_class S G]
{a b : G} :
@[simp]
theorem
inv_coe_set
{G : Type u_1}
[group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : subgroup_class S G] :
@[simp]
theorem
neg_coe_set
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G] :
@[simp]
theorem
exists_neg_mem_iff_exists_mem
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G]
{P : G → Prop} :
@[simp]
theorem
exists_inv_mem_iff_exists_mem
{G : Type u_1}
[group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : subgroup_class S G]
{P : G → Prop} :
theorem
add_mem_cancel_right
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G]
{x y : G}
(h : x ∈ H) :
theorem
mul_mem_cancel_right
{G : Type u_1}
[group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : subgroup_class S G]
{x y : G}
(h : x ∈ H) :
theorem
add_mem_cancel_left
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G]
{x y : G}
(h : x ∈ H) :
theorem
mul_mem_cancel_left
{G : Type u_1}
[group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : subgroup_class S G]
{x y : G}
(h : x ∈ H) :
@[protected, instance]
def
add_subgroup_class.has_neg
{M : Type u_3}
{S : Type u_4}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S} :
An additive subgroup of a add_group inherits an inverse.
@[protected, instance]
def
subgroup_class.has_inv
{M : Type u_3}
{S : Type u_4}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S} :
A subgroup of a group inherits an inverse.
@[protected, instance]
def
subgroup_class.has_div
{M : Type u_3}
{S : Type u_4}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S} :
A subgroup of a group inherits a division
@[protected, instance]
def
add_subgroup_class.has_sub
{M : Type u_3}
{S : Type u_4}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S} :
An additive subgroup of an add_group inherits a subtraction.
@[protected, instance]
def
add_subgroup_class.has_zsmul
{M : Type u_1}
{S : Type u_2}
[sub_neg_monoid M]
[set_like S M]
[add_subgroup_class S M]
{H : S} :
has_scalar ℤ ↥H
An additive subgroup of an add_group inherits an integer scaling.
@[protected, instance]
def
subgroup_class.has_zpow
{M : Type u_3}
{S : Type u_4}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S} :
A subgroup of a group inherits an integer power.
@[simp, norm_cast]
theorem
add_subgroup_class.coe_neg
{M : Type u_3}
{S : Type u_4}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S}
(x : ↥H) :
@[simp, norm_cast]
theorem
subgroup_class.coe_inv
{M : Type u_3}
{S : Type u_4}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S}
(x : ↥H) :
@[simp, norm_cast]
theorem
subgroup_class.coe_div
{M : Type u_3}
{S : Type u_4}
[div_inv_monoid M]
[set_like S M]
[hSM : subgroup_class S M]
{H : S}
(x y : ↥H) :
@[simp, norm_cast]
theorem
add_subgroup_class.coe_sub
{M : Type u_3}
{S : Type u_4}
[sub_neg_monoid M]
[set_like S M]
[hSM : add_subgroup_class S M]
{H : S}
(x y : ↥H) :
@[protected, instance]
def
subgroup_class.to_group
{G : Type u_1}
[group G]
{S : Type u_4}
(H : S)
[set_like S G]
[hSG : subgroup_class S G] :
A subgroup of a group inherits a group structure.
Equations
- subgroup_class.to_group H = function.injective.group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup_class.to_add_group
{G : Type u_1}
[add_group G]
{S : Type u_4}
(H : S)
[set_like S G]
[hSG : add_subgroup_class S G] :
An additive subgroup of an add_group inherits an add_group structure.
Equations
- add_subgroup_class.to_add_group H = function.injective.add_group coe _ _ _ _ _ _ _
@[protected, instance]
def
subgroup_class.to_comm_group
{S : Type u_4}
(H : S)
{G : Type u_1}
[comm_group G]
[set_like S G]
[subgroup_class S G] :
A subgroup of a comm_group is a comm_group.
Equations
- subgroup_class.to_comm_group H = function.injective.comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup_class.to_add_comm_group
{S : Type u_4}
(H : S)
{G : Type u_1}
[add_comm_group G]
[set_like S G]
[add_subgroup_class S G] :
An additive subgroup of an add_comm_group is an add_comm_group.
Equations
- add_subgroup_class.to_add_comm_group H = function.injective.add_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup_class.to_ordered_add_comm_group
{S : Type u_4}
(H : S)
{G : Type u_1}
[ordered_add_comm_group G]
[set_like S G]
[add_subgroup_class S G] :
An additive subgroup of an add_ordered_comm_group is an add_ordered_comm_group.
Equations
@[protected, instance]
def
subgroup_class.to_ordered_comm_group
{S : Type u_4}
(H : S)
{G : Type u_1}
[ordered_comm_group G]
[set_like S G]
[subgroup_class S G] :
A subgroup of an ordered_comm_group is an ordered_comm_group.
Equations
@[protected, instance]
def
add_subgroup_class.to_linear_ordered_add_comm_group
{S : Type u_4}
(H : S)
{G : Type u_1}
[linear_ordered_add_comm_group G]
[set_like S G]
[add_subgroup_class S G] :
An additive subgroup of a linear_ordered_add_comm_group is a
linear_ordered_add_comm_group.
Equations
@[protected, instance]
def
subgroup_class.to_linear_ordered_comm_group
{S : Type u_4}
(H : S)
{G : Type u_1}
[linear_ordered_comm_group G]
[set_like S G]
[subgroup_class S G] :
A subgroup of a linear_ordered_comm_group is a linear_ordered_comm_group.
Equations
def
add_subgroup_class.subtype
{G : Type u_1}
[add_group G]
{S : Type u_4}
(H : S)
[set_like S G]
[hSG : add_subgroup_class S G] :
The natural group hom from an additive subgroup of add_group G to G.
Equations
- add_subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}
def
subgroup_class.subtype
{G : Type u_1}
[group G]
{S : Type u_4}
(H : S)
[set_like S G]
[hSG : subgroup_class S G] :
The natural group hom from a subgroup of group G to G.
Equations
- subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}
@[simp]
theorem
add_subgroup_class.coe_subtype
{G : Type u_1}
[add_group G]
{S : Type u_4}
(H : S)
[set_like S G]
[hSG : add_subgroup_class S G] :
@[simp]
theorem
subgroup_class.coe_subtype
{G : Type u_1}
[group G]
{S : Type u_4}
(H : S)
[set_like S G]
[hSG : subgroup_class S G] :
def
add_subgroup_class.inclusion
{G : Type u_1}
[add_group G]
{S : Type u_4}
[set_like S G]
[hSG : add_subgroup_class S G]
{H K : S}
(h : H ≤ K) :
The inclusion homomorphism from a additive subgroup H contained in K to K.
Equations
- add_subgroup_class.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
def
subgroup_class.inclusion
{G : Type u_1}
[group G]
{S : Type u_4}
[set_like S G]
[hSG : subgroup_class S G]
{H K : S}
(h : H ≤ K) :
The inclusion homomorphism from a subgroup H contained in K to K.
Equations
- subgroup_class.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
@[simp]
theorem
add_subgroup_class.inclusion_self
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : add_subgroup_class S G]
(x : ↥H) :
@[simp]
theorem
subgroup_class.inclusion_self
{G : Type u_1}
[group G]
{S : Type u_4}
{H : S}
[set_like S G]
[hSG : subgroup_class S G]
(x : ↥H) :
⇑(subgroup_class.inclusion le_rfl) x = x
@[simp]
theorem
add_subgroup_class.inclusion_mk
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H K : S}
[set_like S G]
[hSG : add_subgroup_class S G]
{h : H ≤ K}
(x : G)
(hx : x ∈ H) :
⇑(add_subgroup_class.inclusion h) ⟨x, hx⟩ = ⟨x, _⟩
@[simp]
theorem
subgroup_class.inclusion_mk
{G : Type u_1}
[group G]
{S : Type u_4}
{H K : S}
[set_like S G]
[hSG : subgroup_class S G]
{h : H ≤ K}
(x : G)
(hx : x ∈ H) :
⇑(subgroup_class.inclusion h) ⟨x, hx⟩ = ⟨x, _⟩
theorem
subgroup_class.inclusion_right
{G : Type u_1}
[group G]
{S : Type u_4}
{H K : S}
[set_like S G]
[hSG : subgroup_class S G]
(h : H ≤ K)
(x : ↥K)
(hx : ↑x ∈ H) :
⇑(subgroup_class.inclusion h) ⟨↑x, hx⟩ = x
theorem
add_subgroup_class.inclusion_right
{G : Type u_1}
[add_group G]
{S : Type u_4}
{H K : S}
[set_like S G]
[hSG : add_subgroup_class S G]
(h : H ≤ K)
(x : ↥K)
(hx : ↑x ∈ H) :
⇑(add_subgroup_class.inclusion h) ⟨↑x, hx⟩ = x
@[simp]
theorem
subgroup_class.inclusion_inclusion
{G : Type u_1}
[group G]
{S : Type u_4}
{H K : S}
[set_like S G]
[hSG : subgroup_class S G]
{L : S}
(hHK : H ≤ K)
(hKL : K ≤ L)
(x : ↥H) :
⇑(subgroup_class.inclusion hKL) (⇑(subgroup_class.inclusion hHK) x) = ⇑(subgroup_class.inclusion _) x
@[simp]
theorem
add_subgroup_class.coe_inclusion
{G : Type u_1}
[add_group G]
{S : Type u_4}
[set_like S G]
[hSG : add_subgroup_class S G]
{H K : S}
{h : H ≤ K}
(a : ↥H) :
↑(⇑(add_subgroup_class.inclusion h) a) = ↑a
@[simp]
theorem
subgroup_class.coe_inclusion
{G : Type u_1}
[group G]
{S : Type u_4}
[set_like S G]
[hSG : subgroup_class S G]
{H K : S}
{h : H ≤ K}
(a : ↥H) :
↑(⇑(subgroup_class.inclusion h) a) = ↑a
@[simp]
theorem
add_subgroup_class.subtype_comp_inclusion
{G : Type u_1}
[add_group G]
{S : Type u_4}
[set_like S G]
[hSG : add_subgroup_class S G]
{H K : S}
(hH : H ≤ K) :
@[simp]
theorem
subgroup_class.subtype_comp_inclusion
{G : Type u_1}
[group G]
{S : Type u_4}
[set_like S G]
[hSG : subgroup_class S G]
{H K : S}
(hH : H ≤ K) :
- carrier : set G
- mul_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
- one_mem' : 1 ∈ self.carrier
- inv_mem' : ∀ {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier
A subgroup of a group G is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
Instances for subgroup
- subgroup.has_sizeof_inst
- subgroup.set_like
- subgroup.subgroup_class
- subgroup.has_top
- subgroup.has_bot
- subgroup.inhabited
- subgroup.has_inf
- subgroup.has_Inf
- subgroup.complete_lattice
- subgroup.unique
- subgroup.nontrivial
- subgroup.is_modular_lattice
- is_simple_group.subgroup.is_simple_order
- quotient_group.subgroup.has_quotient
- subgroup.pointwise_central_scalar
- subgroup.commutator
- open_subgroup.has_coe_subgroup
- sylow.subgroup.has_coe
- carrier : set G
- add_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
- zero_mem' : 0 ∈ self.carrier
- neg_mem' : ∀ {x : G}, x ∈ self.carrier → -x ∈ self.carrier
An additive subgroup of an additive group G is a subset containing 0, closed
under addition and additive inverse.
Instances for add_subgroup
- add_subgroup.has_sizeof_inst
- add_subgroup.set_like
- add_subgroup.add_subgroup_class
- add_subgroup.has_top
- add_subgroup.has_bot
- add_subgroup.inhabited
- add_subgroup.has_inf
- add_subgroup.has_Inf
- add_subgroup.complete_lattice
- add_subgroup.unique
- add_subgroup.nontrivial
- add_subgroup.is_modular_lattice
- is_simple_add_group.subgroup.is_simple_order
- quotient_add_group.subgroup.has_quotient
- add_subgroup.pointwise_central_scalar
- open_add_subgroup.has_coe_add_subgroup
Reinterpret an add_subgroup as an add_submonoid.
@[protected, instance]
Equations
- subgroup.set_like = {coe := subgroup.carrier _inst_1, coe_injective' := _}
@[protected, instance]
Equations
- add_subgroup.set_like = {coe := add_subgroup.carrier _inst_1, coe_injective' := _}
@[protected, instance]
Equations
- add_subgroup.add_subgroup_class = {to_add_submonoid_class := {to_add_mem_class := {add_mem := _}, zero_mem := _}, neg_mem := _}
@[protected, instance]
Equations
- subgroup.subgroup_class = {to_submonoid_class := {to_mul_mem_class := {mul_mem := _}, one_mem := _}, inv_mem := _}
@[simp]
See Note [custom simps projection]
Equations
- subgroup.simps.coe S = ↑S
See Note [custom simps projection]
Equations
@[simp]
theorem
add_subgroup.coe_to_add_submonoid
{G : Type u_1}
[add_group G]
(K : add_subgroup G) :
↑(K.to_add_submonoid) = ↑K
@[simp]
theorem
subgroup.coe_to_submonoid
{G : Type u_1}
[group G]
(K : subgroup G) :
↑(K.to_submonoid) = ↑K
@[simp]
theorem
subgroup.mem_to_submonoid
{G : Type u_1}
[group G]
(K : subgroup G)
(x : G) :
x ∈ K.to_submonoid ↔ x ∈ K
@[simp]
theorem
add_subgroup.mem_to_add_submonoid
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
(x : G) :
x ∈ K.to_add_submonoid ↔ x ∈ K
@[protected, instance]
def
subgroup.fintype
{G : Type u_1}
[group G]
(K : subgroup G)
[d : decidable_pred (λ (_x : G), _x ∈ K)]
[fintype G] :
Equations
- K.fintype = show fintype {g // g ∈ K}, from infer_instance
@[protected, instance]
def
add_subgroup.fintype
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
[d : decidable_pred (λ (_x : G), _x ∈ K)]
[fintype G] :
Equations
- K.fintype = show fintype {g // g ∈ K}, from infer_instance
@[simp]
theorem
add_subgroup.to_add_submonoid_eq
{G : Type u_1}
[add_group G]
{p q : add_subgroup G} :
p.to_add_submonoid = q.to_add_submonoid ↔ p = q
@[simp]
theorem
subgroup.to_submonoid_eq
{G : Type u_1}
[group G]
{p q : subgroup G} :
p.to_submonoid = q.to_submonoid ↔ p = q
@[simp]
theorem
add_subgroup.to_add_submonoid_le
{G : Type u_1}
[add_group G]
{p q : add_subgroup G} :
p.to_add_submonoid ≤ q.to_add_submonoid ↔ p ≤ q
@[simp]
theorem
subgroup.to_submonoid_le
{G : Type u_1}
[group G]
{p q : subgroup G} :
p.to_submonoid ≤ q.to_submonoid ↔ p ≤ q
Conversion to/from additive/multiplicative #
Supgroups of a group G are isomorphic to additive subgroups of additive G.
Equations
- subgroup.to_add_subgroup = {to_equiv := {to_fun := λ (S : subgroup G), {carrier := (⇑submonoid.to_add_submonoid S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, inv_fun := λ (S : add_subgroup (additive G)), {carrier := (⇑add_submonoid.to_submonoid' S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[simp]
@[simp]
theorem
subgroup.to_add_subgroup_symm_apply_coe
{G : Type u_1}
[group G]
(S : add_subgroup (additive G)) :
Additive subgroup of an additive group additive G are isomorphic to subgroup of G.
def
add_subgroup.to_subgroup
{A : Type u_2}
[add_group A] :
add_subgroup A ≃o subgroup (multiplicative A)
Additive supgroups of an additive group A are isomorphic to subgroups of multiplicative A.
Equations
- add_subgroup.to_subgroup = {to_equiv := {to_fun := λ (S : add_subgroup A), {carrier := (⇑add_submonoid.to_submonoid S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, inv_fun := λ (S : subgroup (multiplicative A)), {carrier := (⇑submonoid.to_add_submonoid' S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[simp]
@[simp]
theorem
add_subgroup.to_subgroup_symm_apply_coe
{A : Type u_2}
[add_group A]
(S : subgroup (multiplicative A)) :
def
subgroup.to_add_subgroup'
{A : Type u_2}
[add_group A] :
subgroup (multiplicative A) ≃o add_subgroup A
Subgroups of an additive group multiplicative A are isomorphic to additive subgroups of A.
@[protected]
Copy of a subgroup with a new carrier equal to the old one. Useful to fix definitional
equalities.
@[protected]
Copy of an additive subgroup with a new carrier equal to the old one.
Useful to fix definitional equalities
@[simp]
theorem
add_subgroup.coe_copy
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
(s : set G)
(hs : s = ↑K) :
theorem
add_subgroup.copy_eq
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
(s : set G)
(hs : s = ↑K) :
theorem
add_subgroup.ext
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : ∀ (x : G), x ∈ H ↔ x ∈ K) :
H = K
Two add_subgroups are equal if they have the same elements.
@[protected]
A subgroup contains the group's 1.
@[protected]
An add_subgroup contains the group's 0.
@[protected]
An add_subgroup is closed under addition.
@[protected]
An add_subgroup is closed under inverse.
@[protected]
theorem
add_subgroup.sub_mem
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{x y : G}
(hx : x ∈ H)
(hy : y ∈ H) :
An add_subgroup is closed under subtraction.
@[protected]
@[protected]
@[protected]
@[protected]
theorem
add_subgroup.exists_neg_mem_iff_exists_mem
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{P : G → Prop} :
@[protected]
theorem
add_subgroup.add_mem_cancel_right
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{x y : G}
(h : x ∈ H) :
@[protected]
theorem
add_subgroup.add_mem_cancel_left
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
{x y : G}
(h : x ∈ H) :
@[protected]
Sum of a list of elements in an add_subgroup is in the add_subgroup.
@[protected]
theorem
add_subgroup.multiset_sum_mem
{G : Type u_1}
[add_comm_group G]
(K : add_subgroup G)
(g : multiset G) :
Sum of a multiset of elements in an add_subgroup of an add_comm_group
is in the add_subgroup.
@[protected]
theorem
subgroup.multiset_prod_mem
{G : Type u_1}
[comm_group G]
(K : subgroup G)
(g : multiset G) :
Product of a multiset of elements in a subgroup of a comm_group is in the subgroup.
theorem
add_subgroup.multiset_noncomm_sum_mem
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
(g : multiset G)
(comm : ∀ (x : G), x ∈ g → ∀ (y : G), y ∈ g → add_commute x y) :
(∀ (a : G), a ∈ g → a ∈ K) → g.noncomm_sum comm ∈ K
@[protected]
theorem
add_subgroup.sum_mem
{G : Type u_1}
[add_comm_group G]
(K : add_subgroup G)
{ι : Type u_2}
{t : finset ι}
{f : ι → G}
(h : ∀ (c : ι), c ∈ t → f c ∈ K) :
Sum of elements in an add_subgroup of an add_comm_group indexed by a finset
is in the add_subgroup.
@[protected]
theorem
subgroup.prod_mem
{G : Type u_1}
[comm_group G]
(K : subgroup G)
{ι : Type u_2}
{t : finset ι}
{f : ι → G}
(h : ∀ (c : ι), c ∈ t → f c ∈ K) :
Product of elements of a subgroup of a comm_group indexed by a finset is in the
subgroup.
theorem
add_subgroup.noncomm_sum_mem
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{ι : Type u_2}
{t : finset ι}
{f : ι → G}
(comm : ∀ (x : ι), x ∈ t → ∀ (y : ι), y ∈ t → add_commute (f x) (f y)) :
(∀ (c : ι), c ∈ t → f c ∈ K) → t.noncomm_sum f comm ∈ K
@[protected]
theorem
add_subgroup.nsmul_mem
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{x : G}
(hx : x ∈ K)
(n : ℕ) :
@[protected]
theorem
add_subgroup.zsmul_mem
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{x : G}
(hx : x ∈ K)
(n : ℤ) :
@[protected, instance]
A subgroup of a group inherits a multiplication.
Equations
- H.has_mul = H.to_submonoid.has_mul
@[protected, instance]
A subgroup of a group inherits a 1.
Equations
- H.has_one = H.to_submonoid.has_one
@[protected, instance]
An add_subgroup of an add_group inherits a natural scaling.
@[protected, instance]
An add_subgroup of an add_group inherits an integer scaling.
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem
add_subgroup.coe_mk
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
(x : G)
(hx : x ∈ H) :
@[protected, instance]
A subgroup of a group inherits a group structure.
Equations
- H.to_group = function.injective.group coe _ _ _ _ _ _ _
@[protected, instance]
An add_subgroup of an add_group inherits an add_group structure.
Equations
- H.to_add_group = function.injective.add_group coe _ _ _ _ _ _ _
@[protected, instance]
An add_subgroup of an add_comm_group is an add_comm_group.
Equations
- H.to_add_comm_group = function.injective.add_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
A subgroup of a comm_group is a comm_group.
Equations
- H.to_comm_group = function.injective.comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup.to_ordered_add_comm_group
{G : Type u_1}
[ordered_add_comm_group G]
(H : add_subgroup G) :
An add_subgroup of an add_ordered_comm_group is an add_ordered_comm_group.
Equations
- H.to_ordered_add_comm_group = function.injective.ordered_add_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
A subgroup of an ordered_comm_group is an ordered_comm_group.
Equations
- H.to_ordered_comm_group = function.injective.ordered_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
subgroup.to_linear_ordered_comm_group
{G : Type u_1}
[linear_ordered_comm_group G]
(H : subgroup G) :
A subgroup of a linear_ordered_comm_group is a linear_ordered_comm_group.
Equations
- H.to_linear_ordered_comm_group = function.injective.linear_ordered_comm_group coe _ _ _ _ _ _ _
@[protected, instance]
def
add_subgroup.to_linear_ordered_add_comm_group
{G : Type u_1}
[linear_ordered_add_comm_group G]
(H : add_subgroup G) :
An add_subgroup of a linear_ordered_add_comm_group is a
linear_ordered_add_comm_group.
Equations
The natural group hom from an add_subgroup of add_group G to G.
@[simp]
@[simp, norm_cast]
theorem
subgroup.coe_multiset_prod
{G : Type u_1}
[comm_group G]
(H : subgroup G)
(m : multiset ↥H) :
@[simp, norm_cast]
theorem
add_subgroup.coe_multiset_sum
{G : Type u_1}
[add_comm_group G]
(H : add_subgroup G)
(m : multiset ↥H) :
@[simp, norm_cast]
theorem
add_subgroup.coe_finset_sum
{ι : Type u_1}
{G : Type u_2}
[add_comm_group G]
(H : add_subgroup G)
(f : ι → ↥H)
(s : finset ι) :
The inclusion homomorphism from a additive subgroup H contained in K to K.
Equations
- add_subgroup.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
The inclusion homomorphism from a subgroup H contained in K to K.
Equations
- subgroup.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _
@[simp]
theorem
add_subgroup.coe_inclusion
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
{h : H ≤ K}
(a : ↥H) :
↑(⇑(add_subgroup.inclusion h) a) = ↑a
theorem
add_subgroup.inclusion_injective
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(h : H ≤ K) :
@[simp]
theorem
add_subgroup.subtype_comp_inclusion
{G : Type u_1}
[add_group G]
{H K : add_subgroup G}
(hH : H ≤ K) :
K.subtype.comp (add_subgroup.inclusion hH) = H.subtype
@[simp]
theorem
subgroup.subtype_comp_inclusion
{G : Type u_1}
[group G]
{H K : subgroup G}
(hH : H ≤ K) :
K.subtype.comp (subgroup.inclusion hH) = H.subtype
@[protected, instance]
The add_subgroup G of the add_group G.
@[simp]
@[simp]
theorem
subgroup.top_equiv_symm_apply_coe
{G : Type u_1}
[group G]
(x : G) :
↑(⇑(subgroup.top_equiv.symm) x) = x
The top subgroup is isomorphic to the group.
This is the group version of submonoid.top_equiv.
Equations
@[simp]
theorem
add_subgroup.top_equiv_symm_apply_coe
{G : Type u_1}
[add_group G]
(x : G) :
↑(⇑(add_subgroup.top_equiv.symm) x) = x
The top additive subgroup is isomorphic to the additive group.
This is the additive group version of add_submonoid.top_equiv.
Equations
@[simp]
@[protected, instance]
The trivial add_subgroup {0} of an add_group G.
@[protected, instance]
Equations
@[protected, instance]
Equations
- subgroup.inhabited = {default := ⊥}
@[protected, instance]
Equations
- add_subgroup.has_bot.bot.unique = {to_inhabited := {default := 0}, uniq := _}
@[protected, instance]
Equations
- subgroup.has_bot.bot.unique = {to_inhabited := {default := 1}, uniq := _}
theorem
subgroup.eq_bot_of_subsingleton
{G : Type u_1}
[group G]
(H : subgroup G)
[subsingleton ↥H] :
theorem
add_subgroup.eq_bot_of_subsingleton
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[subsingleton ↥H] :
@[simp]
@[simp]
theorem
subgroup.eq_top_of_card_eq
{G : Type u_1}
[group G]
(H : subgroup G)
[fintype ↥H]
[fintype G]
(h : fintype.card ↥H = fintype.card G) :
theorem
add_subgroup.eq_top_of_card_eq
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype ↥H]
[fintype G]
(h : fintype.card ↥H = fintype.card G) :
theorem
subgroup.eq_top_of_le_card
{G : Type u_1}
[group G]
(H : subgroup G)
[fintype ↥H]
[fintype G]
(h : fintype.card G ≤ fintype.card ↥H) :
theorem
add_subgroup.eq_top_of_le_card
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype ↥H]
[fintype G]
(h : fintype.card G ≤ fintype.card ↥H) :
theorem
add_subgroup.eq_bot_of_card_le
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype ↥H]
(h : fintype.card ↥H ≤ 1) :
theorem
add_subgroup.eq_bot_of_card_eq
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype ↥H]
(h : fintype.card ↥H = 1) :
theorem
add_subgroup.nontrivial_iff_exists_ne_zero
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
nontrivial ↥H ↔ ∃ (x : G) (H : x ∈ H), x ≠ 0
theorem
subgroup.nontrivial_iff_exists_ne_one
{G : Type u_1}
[group G]
(H : subgroup G) :
nontrivial ↥H ↔ ∃ (x : G) (H : x ∈ H), x ≠ 1
theorem
subgroup.bot_or_nontrivial
{G : Type u_1}
[group G]
(H : subgroup G) :
H = ⊥ ∨ nontrivial ↥H
A subgroup is either the trivial subgroup or nontrivial.
theorem
add_subgroup.bot_or_nontrivial
{G : Type u_1}
[add_group G]
(H : add_subgroup G) :
H = ⊥ ∨ nontrivial ↥H
theorem
add_subgroup.card_nonpos_iff_eq_bot
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype ↥H] :
theorem
add_subgroup.pos_card_iff_ne_bot
{G : Type u_1}
[add_group G]
(H : add_subgroup G)
[fintype ↥H] :
@[protected, instance]
The inf of two subgroups is their intersection.
Equations
- subgroup.has_inf = {inf := λ (H₁ H₂ : subgroup G), {carrier := (H₁.to_submonoid ⊓ H₂.to_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}}
@[protected, instance]
The inf of two add_subgroupss is their intersection.
Equations
- add_subgroup.has_inf = {inf := λ (H₁ H₂ : add_subgroup G), {carrier := (H₁.to_add_submonoid ⊓ H₂.to_add_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}
@[simp]
@[simp]
@[protected, instance]
Equations
- add_subgroup.has_Inf = {Inf := λ (s : set (add_subgroup G)), {carrier := ((⨅ (S : add_subgroup G) (H : S ∈ s), S.to_add_submonoid).copy (⋂ (S : add_subgroup G) (H : S ∈ s), ↑S) _).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}
@[protected, instance]
@[simp, norm_cast]
theorem
add_subgroup.coe_Inf
{G : Type u_1}
[add_group G]
(H : set (add_subgroup G)) :
↑(has_Inf.Inf H) = ⋂ (s : add_subgroup G) (H : s ∈ H), ↑s
@[simp]
theorem
add_subgroup.mem_Inf
{G : Type u_1}
[add_group G]
{S : set (add_subgroup G)}
{x : G} :
x ∈ has_Inf.Inf S ↔ ∀ (p : add_subgroup G), p ∈ S → x ∈ p
theorem
add_subgroup.mem_infi
{G : Type u_1}
[add_group G]
{ι : Sort u_2}
{S : ι → add_subgroup G}
{x : G} :
@[simp, norm_cast]
theorem
add_subgroup.coe_infi
{G : Type u_1}
[add_group G]
{ι : Sort u_2}
{S : ι → add_subgroup G} :
@[protected, instance]
Subgroups of a group form a complete lattice.
Equations
- subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
@[protected, instance]
The add_subgroups of an add_group form a complete lattice.
Equations
- add_subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf add_subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}
theorem
add_subgroup.add_mem_sup
{G : Type u_1}
[add_group G]
{S T : add_subgroup G}
{x y : G}
(hx : x ∈ S)
(hy : y ∈ T) :
theorem
add_subgroup.mem_supr_of_mem
{G : Type u_1}
[add_group G]
{ι : Sort u_2}
{S : ι → add_subgroup G}
(i : ι)
{x : G} :
theorem
subgroup.mem_Sup_of_mem
{G : Type u_1}
[group G]
{S : set (subgroup G)}
{s : subgroup G}
(hs : s ∈ S)
{x : G} :
x ∈ s → x ∈ has_Sup.Sup S
theorem
add_subgroup.mem_Sup_of_mem
{G : Type u_1}
[add_group G]
{S : set (add_subgroup G)}
{s : add_subgroup G}
(hs : s ∈ S)
{x : G} :
x ∈ s → x ∈ has_Sup.Sup S
@[simp]
theorem
subgroup.subsingleton_iff
{G : Type u_1}
[group G] :
subsingleton (subgroup G) ↔ subsingleton G
@[simp]
@[simp]
@[simp]
theorem
add_subgroup.nontrivial_iff
{G : Type u_1}
[add_group G] :
nontrivial (add_subgroup G) ↔ nontrivial G
@[protected, instance]
Equations
- add_subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}
@[protected, instance]
Equations
- subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}
@[protected, instance]
@[protected, instance]
The add_subgroup generated by a set
Equations
- add_subgroup.closure k = has_Inf.Inf {K : add_subgroup G | k ⊆ ↑K}
The subgroup generated by a set.
Equations
- subgroup.closure k = has_Inf.Inf {K : subgroup G | k ⊆ ↑K}
theorem
add_subgroup.mem_closure
{G : Type u_1}
[add_group G]
{k : set G}
{x : G} :
x ∈ add_subgroup.closure k ↔ ∀ (K : add_subgroup G), k ⊆ ↑K → x ∈ K
@[simp]
The subgroup generated by a set includes the set.
@[simp]
theorem
add_subgroup.subset_closure
{G : Type u_1}
[add_group G]
{k : set G} :
k ⊆ ↑(add_subgroup.closure k)
The add_subgroup generated by a set includes the set.
theorem
add_subgroup.not_mem_of_not_mem_closure
{G : Type u_1}
[add_group G]
{k : set G}
{P : G}
(hP : P ∉ add_subgroup.closure k) :
P ∉ k
theorem
subgroup.not_mem_of_not_mem_closure
{G : Type u_1}
[group G]
{k : set G}
{P : G}
(hP : P ∉ subgroup.closure k) :
P ∉ k
@[simp]
theorem
add_subgroup.closure_le
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{k : set G} :
add_subgroup.closure k ≤ K ↔ k ⊆ ↑K
An additive subgroup K includes closure k if and only if it includes k
theorem
subgroup.closure_eq_of_le
{G : Type u_1}
[group G]
(K : subgroup G)
{k : set G}
(h₁ : k ⊆ ↑K)
(h₂ : K ≤ subgroup.closure k) :
subgroup.closure k = K
theorem
add_subgroup.closure_eq_of_le
{G : Type u_1}
[add_group G]
(K : add_subgroup G)
{k : set G}
(h₁ : k ⊆ ↑K)
(h₂ : K ≤ add_subgroup.closure k) :
theorem
subgroup.closure_induction
{G : Type u_1}
[group G]
{k : set G}
{p : G → Prop}
{x : G}
(h : x ∈ subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → p x)
(H1 : p 1)
(Hmul : ∀ (x y : G), p x → p y → p (x * y))
(Hinv : ∀ (x : G), p x → p x⁻¹) :
p x
An induction principle for closure membership. If p holds for 1 and all elements of k, and
is preserved under multiplication and inverse, then p holds for all elements of the closure
of k.
theorem
add_subgroup.closure_induction
{G : Type u_1}
[add_group G]
{k : set G}
{p : G → Prop}
{x : G}
(h : x ∈ add_subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → p x)
(H1 : p 0)
(Hmul : ∀ (x y : G), p x → p y → p (x + y))
(Hinv : ∀ (x : G), p x → p (-x)) :
p x
An induction principle for additive closure membership. If p
holds for 0 and all elements of k, and is preserved under addition and inverses, then p holds
for all elements of the additive closure of k.
theorem
subgroup.closure_induction'
{G : Type u_1}
[group G]
{k : set G}
{p : Π (x : G), x ∈ subgroup.closure k → Prop}
(Hs : ∀ (x : G) (h : x ∈ k), p x _)
(H1 : p 1 _)
(Hmul : ∀ (x : G) (hx : x ∈ subgroup.closure k) (y : G) (hy : y ∈ subgroup.closure k), p x hx → p y hy → p (x * y) _)
(Hinv : ∀ (x : G) (hx : x ∈ subgroup.closure k), p x hx → p x⁻¹ _)
{x : G}
(hx : x ∈ subgroup.closure k) :
p x hx
A dependent version of subgroup.closure_induction.
theorem
add_subgroup.closure_induction'
{G : Type u_1}
[add_group G]
{k : set G}
{p : Π (x : G), x ∈ add_subgroup.closure k → Prop}
(Hs : ∀ (x : G) (h : x ∈ k), p x _)
(H1 : p 0 _)
(Hmul : ∀ (x : G) (hx : x ∈ add_subgroup.closure k) (y : G) (hy : y ∈ add_subgroup.closure k), p x hx → p y hy → p (x + y) _)
(Hinv : ∀ (x : G) (hx : x ∈ add_subgroup.closure k), p x hx → p (-x) _)
{x : G}
(hx : x ∈ add_subgroup.closure k) :
p x hx
A dependent version of add_subgroup.closure_induction.
theorem
add_subgroup.closure_induction₂
{G : Type u_1}
[add_group G]
{k : set G}
{p : G → G → Prop}
{x y : G}
(hx : x ∈ add_subgroup.closure k)
(hy : y ∈ add_subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → p x y)
(H1_left : ∀ (x : G), p 0 x)
(H1_right : ∀ (x : G), p x 0)
(Hmul_left : ∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ + x₂) y)
(Hmul_right : ∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ + y₂))
(Hinv_left : ∀ (x y : G), p x y → p (-x) y)
(Hinv_right : ∀ (x y : G), p x y → p x (-y)) :
p x y
An induction principle for additive closure membership, for predicates with two arguments.
theorem
subgroup.closure_induction₂
{G : Type u_1}
[group G]
{k : set G}
{p : G → G → Prop}
{x y : G}
(hx : x ∈ subgroup.closure k)
(hy : y ∈ subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → p x y)
(H1_left : ∀ (x : G), p 1 x)
(H1_right : ∀ (x : G), p x 1)
(Hmul_left : ∀ (x₁ x₂ y : G), p x₁ y → p x₂ y → p (x₁ * x₂) y)
(Hmul_right : ∀ (x y₁ y₂ : G), p x y₁ → p x y₂ → p x (y₁ * y₂))
(Hinv_left : ∀ (x y : G), p x y → p x⁻¹ y)
(Hinv_right : ∀ (x y : G), p x y → p x y⁻¹) :
p x y
An induction principle for closure membership for predicates with two arguments.
@[simp]
theorem
subgroup.closure_closure_coe_preimage
{G : Type u_1}
[group G]
{k : set G} :
subgroup.closure (coe ⁻¹' k) = ⊤
@[simp]
theorem
add_subgroup.closure_closure_coe_preimage
{G : Type u_1}
[add_group G]
{k : set G} :
add_subgroup.closure (coe ⁻¹' k) = ⊤
def
subgroup.closure_comm_group_of_comm
{G : Type u_1}
[group G]
{k : set G}
(hcomm : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → x * y = y * x) :
If all the elements of a set s commute, then closure s is a commutative group.
Equations
- subgroup.closure_comm_group_of_comm hcomm = {mul := group.mul (subgroup.closure k).to_group, mul_assoc := _, one := group.one (subgroup.closure k).to_group, one_mul := _, mul_one := _, npow := group.npow (subgroup.closure k).to_group, npow_zero' := _, npow_succ' := _, inv := group.inv (subgroup.closure k).to_group, div := group.div (subgroup.closure k).to_group, div_eq_mul_inv := _, zpow := group.zpow (subgroup.closure k).to_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
def
add_subgroup.closure_add_comm_group_of_comm
{G : Type u_1}
[add_group G]
{k : set G}
(hcomm : ∀ (x : G), x ∈ k → ∀ (y : G), y ∈ k → x + y = y + x) :
If all the elements of a set s commute, then closure s is an additive
commutative group.
Equations
- add_subgroup.closure_add_comm_group_of_comm hcomm = {add := add_group.add (add_subgroup.closure k).to_add_group, add_assoc := _, zero := add_group.zero (add_subgroup.closure k).to_add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul (add_subgroup.closure k).to_add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (add_subgroup.closure k).to_add_group, sub := add_group.sub (add_subgroup.closure k).to_add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul (add_subgroup.closure k).to_add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected]
closure forms a Galois insertion with the coercion to set.
Equations
- add_subgroup.gi G = {choice := λ (s : set G) (_x : ↑(add_subgroup.closure s) ≤ s), add_subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}
@[protected]
closure forms a Galois insertion with the coercion to set.
Equations
- subgroup.gi G = {choice := λ (s : set G) (_x : ↑(subgroup.closure s) ≤ s), subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}
@[simp]
Closure of a subgroup K equals K.
@[simp]
Additive closure of an additive subgroup K equals K
@[simp]
@[simp]
@[simp]
theorem
subgroup.closure_union
{G : Type u_1}
[group G]
(s t : set G) :
subgroup.closure (s ∪ t) = subgroup.closure s ⊔ subgroup.closure t
theorem
subgroup.closure_Union
{G : Type u_1}
[group G]
{ι : Sort u_2}
(s : ι → set G) :
subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), subgroup.closure (s i)
theorem
add_subgroup.closure_Union
{G : Type u_1}
[add_group G]
{ι : Sort u_2}
(s : ι → set G) :
add_subgroup.closure (⋃ (i : ι), s i) = ⨆ (i : ι), add_subgroup.closure (s i)
theorem
subgroup.closure_eq_bot_iff
(G : Type u_1)
[group G]
(S : set G) :
subgroup.closure S = ⊥ ↔ S ⊆ {1}
theorem
add_subgroup.closure_eq_bot_iff
(G : Type u_1)
[add_group G]
(S : set G) :
add_subgroup.closure S = ⊥ ↔ S ⊆ {0}
theorem
subgroup.supr_eq_closure
{G : Type u_1}
[group G]
{ι : Sort u_2}
(p : ι → subgroup G) :
(⨆ (i : ι), p i) = subgroup.closure (⋃ (i : ι), ↑(p i))
theorem
add_subgroup.supr_eq_closure
{G : Type u_1}
[add_group G]
{ι : Sort u_2}
(p : ι → add_subgroup G) :
(⨆ (i : ι), p i) = add_subgroup.closure (⋃ (i : ι), ↑(p i))
The add_subgroup generated by an element of an add_group equals the set of
natural number multiples of the element.
The subgroup generated by an element of a group equals the set of integer number powers of the element.
theorem
add_subgroup.closure_singleton_zero
{G : Type u_1}
[add_group G] :
add_subgroup.closure {0} = ⊥
@[simp]
theorem
subgroup.inv_subset_closure
{G : Type u_1}
[group G]
(S : set G) :
S⁻¹ ⊆ ↑(subgroup.closure S)
@[simp]
theorem
add_subgroup.neg_subset_closure
{G : Type u_1}
[add_group G]
(S : set G) :
-S ⊆ ↑(add_subgroup.closure S)
@[simp]
@[simp]
theorem
subgroup.closure_to_submonoid
{G : Type u_1}
[group G]
(S : set G) :
(subgroup.closure S).to_submonoid = submonoid.closure (S ∪ S⁻¹)
theorem
subgroup.closure_induction''
{G : Type u_1}
[group G]
{k : set G}
{p : G → Prop}
{x : G}
(h : x ∈ subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → p x)
(Hk_inv : ∀ (x : G), x ∈ k → p x⁻¹)
(H1 : p 1)
(Hmul : ∀ (x y : G), p x → p y → p (x * y)) :
p x
An induction principle for closure membership. If p holds for 1 and all elements of
k and their inverse, and is preserved under multiplication, then p holds for all elements of
the closure of k.
theorem
add_subgroup.closure_induction''
{G : Type u_1}
[add_group G]
{k : set G}
{p : G → Prop}
{x : G}
(h : x ∈ add_subgroup.closure k)
(Hk : ∀ (x : G), x ∈ k → p x)
(Hk_inv : ∀ (x : G), x ∈ k → p (-x))
(H1 : p 0)
(Hmul : ∀ (x y : G), p x → p y → p (x + y)) :