mathlib documentation

group_theory.subgroup.basic

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:

Definitions in the file:

Implementation notes #

Subgroup inclusion is denoted rather than , although is defined as membership of a subgroup's underlying set.

Tags #

subgroup, subgroups

@[class]
structure inv_mem_class (S : Type u_3) (G : Type u_4) [has_inv G] [set_like S G] :
Type
  • inv_mem : ∀ {s : S} {x : G}, x sx⁻¹ s

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]
structure neg_mem_class (S : Type u_3) (G : Type u_4) [has_neg G] [set_like S G] :
Type
  • neg_mem : ∀ {s : S} {x : G}, x s-x s

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]
structure subgroup_class (S : Type u_3) (G : Type u_4) [div_inv_monoid G] [set_like S G] :
Type

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]
structure add_subgroup_class (S : Type u_3) (G : Type u_4) [sub_neg_monoid G] [set_like S G] :
Type

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] :
Equations
@[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] :
Equations
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) :
x / 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) :
x - 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 : ) :
x ^ n K
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 : ) :
n x K
@[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} :
-x H x H
@[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} :
x⁻¹ H x H
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} :
a - b H b - a H
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} :
a / b H b / a H
@[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} :
(∃ (x : G), x H P (-x)) ∃ (x : G) (H : x H), P x
@[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} :
(∃ (x : G), x H P x⁻¹) ∃ (x : G) (H : x H), P x
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) :
y + x H y 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) :
y * x H y 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) :
x + y H y 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) :
x * y H y 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.

Equations
@[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.

Equations
@[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

Equations
@[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.

Equations
@[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} :

An additive subgroup of an add_group inherits an integer scaling.

Equations
@[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.

Equations
@[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) :
(x / y) = x / y
@[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) :
(x - y) = x - y
@[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
@[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
@[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
@[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
@[protected, instance]

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
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
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
@[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] :
@[simp, norm_cast]
theorem add_subgroup_class.coe_smul {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) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem subgroup_class.coe_pow {G : Type u_1} [group G] {S : Type u_4} {H : S} [set_like S G] [hSG : subgroup_class S G] (x : H) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem add_subgroup_class.coe_zsmul {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) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem subgroup_class.coe_zpow {G : Type u_1} [group G] {S : Type u_4} {H : S} [set_like S G] [hSG : subgroup_class S G] (x : H) (n : ) :
(x ^ n) = x ^ n
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
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
@[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) :
@[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) :
@[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) :
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) :
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) :
@[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) :
@[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) :
@[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) :
@[simp]
@[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) :
def subgroup.to_submonoid {G : Type u_3} [group G] (self : subgroup G) :

Reinterpret a subgroup as a submonoid.

structure subgroup (G : Type u_3) [group G] :
Type u_3

A subgroup of a group G is a subset containing 1, closed under multiplication and closed under multiplicative inverse.

Instances for subgroup
structure add_subgroup (G : Type u_3) [add_group G] :
Type u_3

An additive subgroup of an additive group G is a subset containing 0, closed under addition and additive inverse.

Instances for add_subgroup
def add_subgroup.to_add_submonoid {G : Type u_3} [add_group G] (self : add_subgroup G) :

Reinterpret an add_subgroup as an add_submonoid.

@[protected, instance]
def subgroup.set_like {G : Type u_1} [group G] :
Equations
@[protected, instance]
def add_subgroup.set_like {G : Type u_1} [add_group G] :
Equations
@[protected, instance]
def subgroup.subgroup_class {G : Type u_1} [group G] :
Equations
@[simp]
theorem subgroup.mem_carrier {G : Type u_1} [group G] {s : subgroup G} {x : G} :
x s.carrier x s
@[simp]
theorem add_subgroup.mem_carrier {G : Type u_1} [add_group G] {s : add_subgroup G} {x : G} :
x s.carrier x s
@[simp]
theorem add_subgroup.mem_mk {G : Type u_1} [add_group G] {s : set G} {x : G} (h_one : ∀ {a b : G}, a sb sa + b s) (h_mul : 0 s) (h_inv : ∀ {x : G}, x s-x s) :
x {carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv} x s
@[simp]
theorem subgroup.mem_mk {G : Type u_1} [group G] {s : set G} {x : G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : 1 s) (h_inv : ∀ {x : G}, x sx⁻¹ s) :
x {carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv} x s
@[simp]
theorem subgroup.coe_set_mk {G : Type u_1} [group G] {s : set G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : 1 s) (h_inv : ∀ {x : G}, x sx⁻¹ s) :
{carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv} = s
@[simp]
theorem add_subgroup.coe_set_mk {G : Type u_1} [add_group G] {s : set G} (h_one : ∀ {a b : G}, a sb sa + b s) (h_mul : 0 s) (h_inv : ∀ {x : G}, x s-x s) :
{carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv} = s
@[simp]
theorem add_subgroup.mk_le_mk {G : Type u_1} [add_group G] {s t : set G} (h_one : ∀ {a b : G}, a sb sa + b s) (h_mul : 0 s) (h_inv : ∀ {x : G}, x s-x s) (h_one' : ∀ {a b : G}, a tb ta + b t) (h_mul' : 0 t) (h_inv' : ∀ {x : G}, x t-x t) :
{carrier := s, add_mem' := h_one, zero_mem' := h_mul, neg_mem' := h_inv} {carrier := t, add_mem' := h_one', zero_mem' := h_mul', neg_mem' := h_inv'} s t
@[simp]
theorem subgroup.mk_le_mk {G : Type u_1} [group G] {s t : set G} (h_one : ∀ {a b : G}, a sb sa * b s) (h_mul : 1 s) (h_inv : ∀ {x : G}, x sx⁻¹ s) (h_one' : ∀ {a b : G}, a tb ta * b t) (h_mul' : 1 t) (h_inv' : ∀ {x : G}, x tx⁻¹ t) :
{carrier := s, mul_mem' := h_one, one_mem' := h_mul, inv_mem' := h_inv} {carrier := t, mul_mem' := h_one', one_mem' := h_mul', inv_mem' := h_inv'} s t
def subgroup.simps.coe {G : Type u_1} [group G] (S : subgroup G) :
set G

See Note [custom simps projection]

Equations
@[simp]
@[simp]
theorem subgroup.coe_to_submonoid {G : Type u_1} [group G] (K : subgroup G) :
@[simp]
theorem subgroup.mem_to_submonoid {G : Type u_1} [group G] (K : subgroup G) (x : G) :
@[simp]
theorem add_subgroup.mem_to_add_submonoid {G : Type u_1} [add_group G] (K : add_subgroup G) (x : G) :
@[protected, instance]
def subgroup.fintype {G : Type u_1} [group G] (K : subgroup G) [d : decidable_pred (λ (_x : G), _x K)] [fintype G] :
Equations
@[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
@[simp]
@[simp]
theorem subgroup.to_submonoid_eq {G : Type u_1} [group G] {p q : subgroup G} :
@[simp]
theorem subgroup.to_submonoid_le {G : Type u_1} [group G] {p q : subgroup G} :

Conversion to/from additive/multiplicative #

Supgroups of a group G are isomorphic to additive subgroups of additive G.

Equations
@[reducible]

Additive subgroup of an additive group additive G are isomorphic to subgroup of G.

Additive supgroups of an additive group A are isomorphic to subgroups of multiplicative A.

Equations
@[reducible]

Subgroups of an additive group multiplicative A are isomorphic to additive subgroups of A.

@[protected]
def subgroup.copy {G : Type u_1} [group G] (K : subgroup G) (s : set G) (hs : s = K) :

Copy of a subgroup with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations
@[protected]
def add_subgroup.copy {G : Type u_1} [add_group G] (K : add_subgroup G) (s : set G) (hs : s = K) :

Copy of an additive subgroup with a new carrier equal to the old one. Useful to fix definitional equalities

Equations
@[simp]
theorem add_subgroup.coe_copy {G : Type u_1} [add_group G] (K : add_subgroup G) (s : set G) (hs : s = K) :
(K.copy s hs) = s
@[simp]
theorem subgroup.coe_copy {G : Type u_1} [group G] (K : subgroup G) (s : set G) (hs : s = K) :
(K.copy s hs) = s
theorem add_subgroup.copy_eq {G : Type u_1} [add_group G] (K : add_subgroup G) (s : set G) (hs : s = K) :
K.copy s hs = K
theorem subgroup.copy_eq {G : Type u_1} [group G] (K : subgroup G) (s : set G) (hs : s = K) :
K.copy s hs = K
@[ext]
theorem subgroup.ext {G : Type u_1} [group G] {H K : subgroup G} (h : ∀ (x : G), x H x K) :
H = K

Two subgroups are equal if they have the same elements.

@[ext]
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]
theorem subgroup.one_mem {G : Type u_1} [group G] (H : subgroup G) :
1 H

A subgroup contains the group's 1.

@[protected]
theorem add_subgroup.zero_mem {G : Type u_1} [add_group G] (H : add_subgroup G) :
0 H

An add_subgroup contains the group's 0.

@[protected]
theorem add_subgroup.add_mem {G : Type u_1} [add_group G] (H : add_subgroup G) {x y : G} :
x Hy Hx + y H

An add_subgroup is closed under addition.

@[protected]
theorem subgroup.mul_mem {G : Type u_1} [group G] (H : subgroup G) {x y : G} :
x Hy Hx * y H

A subgroup is closed under multiplication.

@[protected]
theorem subgroup.inv_mem {G : Type u_1} [group G] (H : subgroup G) {x : G} :
x Hx⁻¹ H

A subgroup is closed under inverse.

@[protected]
theorem add_subgroup.neg_mem {G : Type u_1} [add_group G] (H : add_subgroup G) {x : G} :
x H-x H

An add_subgroup is closed under inverse.

@[protected]
theorem subgroup.div_mem {G : Type u_1} [group G] (H : subgroup G) {x y : G} (hx : x H) (hy : y H) :
x / y H

A subgroup is closed under division.

@[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) :
x - y H

An add_subgroup is closed under subtraction.

@[protected]
theorem add_subgroup.neg_mem_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {x : G} :
-x H x H
@[protected]
theorem subgroup.inv_mem_iff {G : Type u_1} [group G] (H : subgroup G) {x : G} :
x⁻¹ H x H
@[protected]
theorem add_subgroup.sub_mem_comm_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {a b : G} :
a - b H b - a H
@[protected]
theorem subgroup.div_mem_comm_iff {G : Type u_1} [group G] (H : subgroup G) {a b : G} :
a / b H b / a H
@[protected]
theorem add_subgroup.neg_coe_set {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[protected]
theorem subgroup.inv_coe_set {G : Type u_1} [group G] (H : subgroup G) :
@[protected]
theorem subgroup.exists_inv_mem_iff_exists_mem {G : Type u_1} [group G] (K : subgroup G) {P : G → Prop} :
(∃ (x : G), x K P x⁻¹) ∃ (x : G) (H : x K), P x
@[protected]
theorem add_subgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {P : G → Prop} :
(∃ (x : G), x K P (-x)) ∃ (x : G) (H : x K), P x
@[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) :
y + x H y H
@[protected]
theorem subgroup.mul_mem_cancel_right {G : Type u_1} [group G] (H : subgroup G) {x y : G} (h : x H) :
y * x H y H
@[protected]
theorem subgroup.mul_mem_cancel_left {G : Type u_1} [group G] (H : subgroup G) {x y : G} (h : x H) :
x * y H y 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) :
x + y H y H
@[protected]
theorem subgroup.list_prod_mem {G : Type u_1} [group G] (K : subgroup G) {l : list G} :
(∀ (x : G), x lx K)l.prod K

Product of a list of elements in a subgroup is in the subgroup.

@[protected]
theorem add_subgroup.list_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {l : list G} :
(∀ (x : G), x lx K)l.sum K

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) :
(∀ (a : G), a ga K)g.sum K

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) :
(∀ (a : G), a ga K)g.prod K

Product of a multiset of elements in a subgroup of a comm_group is in the subgroup.

theorem subgroup.multiset_noncomm_prod_mem {G : Type u_1} [group G] (K : subgroup G) (g : multiset G) (comm : ∀ (x : G), x g∀ (y : G), y gcommute x y) :
(∀ (a : G), a ga K)g.noncomm_prod comm K
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 gadd_commute x y) :
(∀ (a : G), a ga 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 tf c K) :
t.sum (λ (c : ι), 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 tf c K) :
t.prod (λ (c : ι), 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 tadd_commute (f x) (f y)) :
(∀ (c : ι), c tf c K)t.noncomm_sum f comm K
theorem subgroup.noncomm_prod_mem {G : Type u_1} [group G] (K : subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (comm : ∀ (x : ι), x t∀ (y : ι), y tcommute (f x) (f y)) :
(∀ (c : ι), c tf c K)t.noncomm_prod f comm K
@[protected]
theorem subgroup.pow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x K) (n : ) :
x ^ n K
@[protected]
theorem add_subgroup.nsmul_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {x : G} (hx : x K) (n : ) :
n x K
@[protected]
theorem subgroup.zpow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x K) (n : ) :
x ^ n K
@[protected]
theorem add_subgroup.zsmul_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {x : G} (hx : x K) (n : ) :
n x K
def subgroup.of_div {G : Type u_1} [group G] (s : set G) (hsn : s.nonempty) (hs : ∀ (x : G), x s∀ (y : G), y sx * y⁻¹ s) :

Construct a subgroup from a nonempty set that is closed under division.

Equations
def add_subgroup.of_sub {G : Type u_1} [add_group G] (s : set G) (hsn : s.nonempty) (hs : ∀ (x : G), x s∀ (y : G), y sx + -y s) :

Construct a subgroup from a nonempty set that is closed under subtraction

Equations
@[protected, instance]
def subgroup.has_mul {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a multiplication.

Equations
@[protected, instance]
def add_subgroup.has_add {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits an addition.

Equations
@[protected, instance]
def subgroup.has_one {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a 1.

Equations
@[protected, instance]
def add_subgroup.has_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits a zero.

Equations
@[protected, instance]
def add_subgroup.has_neg {G : Type u_1} [add_group G] (H : add_subgroup G) :

A add_subgroup of a add_group inherits an inverse.

Equations
@[protected, instance]
def subgroup.has_inv {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits an inverse.

Equations
@[protected, instance]
def subgroup.has_div {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a division

Equations
@[protected, instance]
def add_subgroup.has_sub {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits a subtraction.

Equations
@[protected, instance]
def add_subgroup.has_nsmul {G : Type u_1} [add_group G] {H : add_subgroup G} :

An add_subgroup of an add_group inherits a natural scaling.

Equations
@[protected, instance]
def subgroup.has_npow {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a natural power

Equations
@[protected, instance]
def add_subgroup.has_zsmul {G : Type u_1} [add_group G] {H : add_subgroup G} :

An add_subgroup of an add_group inherits an integer scaling.

Equations
@[protected, instance]
def subgroup.has_zpow {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits an integer power

Equations
@[simp, norm_cast]
theorem add_subgroup.coe_add {G : Type u_1} [add_group G] (H : add_subgroup G) (x y : H) :
(x + y) = x + y
@[simp, norm_cast]
theorem subgroup.coe_mul {G : Type u_1} [group G] (H : subgroup G) (x y : H) :
(x * y) = x * y
@[simp, norm_cast]
theorem add_subgroup.coe_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
0 = 0
@[simp, norm_cast]
theorem subgroup.coe_one {G : Type u_1} [group G] (H : subgroup G) :
1 = 1
@[simp, norm_cast]
theorem add_subgroup.coe_neg {G : Type u_1} [add_group G] (H : add_subgroup G) (x : H) :
@[simp, norm_cast]
theorem subgroup.coe_inv {G : Type u_1} [group G] (H : subgroup G) (x : H) :
@[simp, norm_cast]
theorem subgroup.coe_div {G : Type u_1} [group G] (H : subgroup G) (x y : H) :
(x / y) = x / y
@[simp, norm_cast]
theorem add_subgroup.coe_sub {G : Type u_1} [add_group G] (H : add_subgroup G) (x y : H) :
(x - y) = x - y
@[simp, norm_cast]
theorem add_subgroup.coe_mk {G : Type u_1} [add_group G] (H : add_subgroup G) (x : G) (hx : x H) :
x, hx⟩ = x
@[simp, norm_cast]
theorem subgroup.coe_mk {G : Type u_1} [group G] (H : subgroup G) (x : G) (hx : x H) :
x, hx⟩ = x
@[simp, norm_cast]
theorem subgroup.coe_pow {G : Type u_1} [group G] (H : subgroup G) (x : H) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem add_subgroup.coe_nsmul {G : Type u_1} [add_group G] (H : add_subgroup G) (x : H) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem add_subgroup.coe_zsmul {G : Type u_1} [add_group G] (H : add_subgroup G) (x : H) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem subgroup.coe_zpow {G : Type u_1} [group G] (H : subgroup G) (x : H) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def subgroup.to_group {G : Type u_1} [group G] (H : subgroup G) :

A subgroup of a group inherits a group structure.

Equations
@[protected, instance]
def add_subgroup.to_add_group {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits an add_group structure.

Equations
@[protected, instance]
def subgroup.to_comm_group {G : Type u_1} [comm_group G] (H : subgroup G) :

A subgroup of a comm_group is a comm_group.

Equations
@[protected, instance]

An add_subgroup of an add_ordered_comm_group is an add_ordered_comm_group.

Equations
@[protected, instance]

A subgroup of an ordered_comm_group is an ordered_comm_group.

Equations
def subgroup.subtype {G : Type u_1} [group G] (H : subgroup G) :

The natural group hom from a subgroup of group G to G.

Equations
def add_subgroup.subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :

The natural group hom from an add_subgroup of add_group G to G.

Equations
@[simp]
theorem subgroup.coe_subtype {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem add_subgroup.coe_subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp, norm_cast]
theorem add_subgroup.coe_list_sum {G : Type u_1} [add_group G] (H : add_subgroup G) (l : list H) :
@[simp, norm_cast]
theorem subgroup.coe_list_prod {G : Type u_1} [group G] (H : subgroup G) (l : list H) :
@[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 ι) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp, norm_cast]
theorem subgroup.coe_finset_prod {ι : Type u_1} {G : Type u_2} [comm_group G] (H : subgroup G) (f : ι → H) (s : finset ι) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
def add_subgroup.inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :

The inclusion homomorphism from a additive subgroup H contained in K to K.

Equations
def subgroup.inclusion {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :

The inclusion homomorphism from a subgroup H contained in K to K.

Equations
@[simp]
theorem subgroup.coe_inclusion {G : Type u_1} [group G] {H K : subgroup G} {h : H K} (a : H) :
@[simp]
theorem add_subgroup.coe_inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} {h : H K} (a : H) :
theorem subgroup.inclusion_injective {G : Type u_1} [group G] {H K : 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) :
@[simp]
theorem subgroup.subtype_comp_inclusion {G : Type u_1} [group G] {H K : subgroup G} (hH : H K) :
@[protected, instance]
def add_subgroup.has_top {G : Type u_1} [add_group G] :

The add_subgroup G of the add_group G.

Equations
@[protected, instance]
def subgroup.has_top {G : Type u_1} [group G] :

The subgroup G of the group G.

Equations
@[simp]
@[simp]
theorem subgroup.top_equiv_symm_apply_coe {G : Type u_1} [group G] (x : G) :
def subgroup.top_equiv {G : Type u_1} [group G] :

The top subgroup is isomorphic to the group.

This is the group version of submonoid.top_equiv.

Equations
@[simp]
def add_subgroup.top_equiv {G : Type u_1} [add_group G] :

The top additive subgroup is isomorphic to the additive group.

This is the additive group version of add_submonoid.top_equiv.

Equations
@[simp]
theorem subgroup.top_equiv_apply {G : Type u_1} [group G] (x : ) :
@[protected, instance]
def add_subgroup.has_bot {G : Type u_1} [add_group G] :

The trivial add_subgroup {0} of an add_group G.

Equations
@[protected, instance]
def subgroup.has_bot {G : Type u_1} [group G] :

The trivial subgroup {1} of an group G.

Equations
@[protected, instance]
def add_subgroup.inhabited {G : Type u_1} [add_group G] :
Equations
@[protected, instance]
def subgroup.inhabited {G : Type u_1} [group G] :
Equations
@[simp]
theorem subgroup.mem_bot {G : Type u_1} [group G] {x : G} :
x x = 1
@[simp]
theorem add_subgroup.mem_bot {G : Type u_1} [add_group G] {x : G} :
x x = 0
@[simp]
theorem add_subgroup.mem_top {G : Type u_1} [add_group G] (x : G) :
@[simp]
theorem subgroup.mem_top {G : Type u_1} [group G] (x : G) :
@[simp]
theorem subgroup.coe_top {G : Type u_1} [group G] :
@[simp]
theorem add_subgroup.coe_top {G : Type u_1} [add_group G] :
@[simp]
theorem add_subgroup.coe_bot {G : Type u_1} [add_group G] :
= {0}
@[simp]
theorem subgroup.coe_bot {G : Type u_1} [group G] :
= {1}
@[protected, instance]
Equations
@[protected, instance]
def subgroup.has_bot.bot.unique {G : Type u_1} [group G] :
Equations
theorem subgroup.eq_bot_iff_forall {G : Type u_1} [group G] (H : subgroup G) :
H = ∀ (x : G), x Hx = 1
theorem add_subgroup.eq_bot_iff_forall {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = ∀ (x : G), x Hx = 0
theorem subgroup.eq_bot_of_subsingleton {G : Type u_1} [group G] (H : subgroup G) [subsingleton H] :
H =
theorem subgroup.coe_eq_univ {G : Type u_1} [group G] {H : subgroup G} :
theorem add_subgroup.coe_eq_univ {G : Type u_1} [add_group G] {H : add_subgroup G} :
theorem add_subgroup.coe_eq_singleton {G : Type u_1} [add_group G] {H : add_subgroup G} :
(∃ (g : G), H = {g}) H =
theorem subgroup.coe_eq_singleton {G : Type u_1} [group G] {H : subgroup G} :
(∃ (g : G), H = {g}) H =
@[protected, instance]
def subgroup.fintype_bot {G : Type u_1} [group G] :
Equations
@[protected, instance]
def add_subgroup.fintype_bot {G : Type u_1} [add_group G] :
Equations
@[simp]
theorem subgroup.card_bot {G : Type u_1} [group G] {_x : fintype } :
@[simp]
theorem add_subgroup.card_bot {G : Type u_1} [add_group G] {_x : fintype } :
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) :
H =
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) :
H =
theorem subgroup.eq_bot_of_card_le {G : Type u_1} [group G] (H : subgroup G) [fintype H] (h : fintype.card H 1) :
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) :
H =
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) :
H =
theorem subgroup.eq_bot_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype H] (h : fintype.card H = 1) :
H =
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) :

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) :

A subgroup is either the trivial subgroup or nontrivial.

theorem subgroup.bot_or_exists_ne_one {G : Type u_1} [group G] (H : subgroup G) :
H = ∃ (x : G) (H : x H), x 1

A subgroup is either the trivial subgroup or contains a non-identity element.

theorem add_subgroup.bot_or_exists_ne_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = ∃ (x : G) (H : x H), x 0

A subgroup is either the trivial subgroup or contains a nonzero element.

theorem subgroup.card_le_one_iff_eq_bot {G : Type u_1} [group G] (H : subgroup G) [fintype H] :
theorem subgroup.one_lt_card_iff_ne_bot {G : Type u_1} [group G] (H : subgroup G) [fintype H] :
@[protected, instance]
def subgroup.has_inf {G : Type u_1} [group G] :

The inf of two subgroups is their intersection.

Equations
@[protected, instance]
def add_subgroup.has_inf {G : Type u_1} [add_group G] :

The inf of two add_subgroupss is their intersection.

Equations
@[simp]
theorem subgroup.coe_inf {G : Type u_1} [group G] (p p' : subgroup G) :
(p p') = p p'
@[simp]
theorem add_subgroup.coe_inf {G : Type u_1} [add_group G] (p p' : add_subgroup G) :
(p p') = p p'
@[simp]
theorem add_subgroup.mem_inf {G : Type u_1} [add_group G] {p p' : add_subgroup G} {x : G} :
x p p' x p x p'
@[simp]
theorem subgroup.mem_inf {G : Type u_1} [group G] {p p' : subgroup G} {x : G} :
x p p' x p x p'
@[protected, instance]
def add_subgroup.has_Inf {G : Type u_1} [add_group G] :
Equations
@[protected, instance]
def subgroup.has_Inf {G : Type u_1} [group G] :
Equations
@[simp, norm_cast]
theorem subgroup.coe_Inf {G : Type u_1} [group G] (H : set (subgroup G)) :
(has_Inf.Inf H) = ⋂ (s : subgroup G) (H : s H), s
@[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 Sx p
@[simp]
theorem subgroup.mem_Inf {G : Type u_1} [group G] {S : set (subgroup G)} {x : G} :
x has_Inf.Inf S ∀ (p : subgroup G), p Sx p
theorem subgroup.mem_infi {G : Type u_1} [group G] {ι : Sort u_2} {S : ι → subgroup G} {x : G} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i
theorem add_subgroup.mem_infi {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι → add_subgroup G} {x : G} :
(x ⨅ (i : ι), S i) ∀ (i : ι), x S i
@[simp, norm_cast]
theorem subgroup.coe_infi {G : Type u_1} [group G] {ι : Sort u_2} {S : ι → subgroup G} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
@[simp, norm_cast]
theorem add_subgroup.coe_infi {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι → add_subgroup G} :
(⨅ (i : ι), S i) = ⋂ (i : ι), (S i)
@[protected, instance]

Subgroups of a group form a complete lattice.

Equations
@[protected, instance]

The add_subgroups of an add_group form a complete lattice.

Equations
theorem subgroup.mem_sup_left {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x Sx S T
theorem add_subgroup.mem_sup_left {G : Type u_1} [add_group G] {S T : add_subgroup G} {x : G} :
x Sx S T
theorem subgroup.mem_sup_right {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x Tx S T
theorem add_subgroup.mem_sup_right {G : Type u_1} [add_group G] {S T : add_subgroup G} {x : G} :
x Tx S T
theorem subgroup.mul_mem_sup {G : Type u_1} [group G] {S T : subgroup G} {x y : G} (hx : x S) (hy : y T) :
x * y S T
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) :
x + y S T
theorem subgroup.mem_supr_of_mem {G : Type u_1} [group G] {ι : Sort u_2} {S : ι → subgroup G} (i : ι) {x : G} :
x S ix supr S
theorem add_subgroup.mem_supr_of_mem {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι → add_subgroup G} (i : ι) {x : G} :
x S ix supr S
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 sx 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 sx has_Sup.Sup S
@[simp]
@[simp]
theorem subgroup.nontrivial_iff {G : Type u_1} [group G] :
@[simp]
@[protected, instance]
def add_subgroup.unique {G : Type u_1} [add_group G] [subsingleton G] :
Equations
@[protected, instance]
def subgroup.unique {G : Type u_1} [group G] [subsingleton G] :
Equations
@[protected, instance]
def subgroup.nontrivial {G : Type u_1} [group G] [nontrivial G] :
@[protected, instance]
theorem add_subgroup.eq_top_iff' {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = ∀ (x : G), x H
theorem subgroup.eq_top_iff' {G : Type u_1} [group G] (H : subgroup G) :
H = ∀ (x : G), x H
def add_subgroup.closure {G : Type u_1} [add_group G] (k : set G) :

The add_subgroup generated by a set

Equations
Instances for add_subgroup.closure
def subgroup.closure {G : Type u_1} [group G] (k : set G) :

The subgroup generated by a set.

Equations
Instances for subgroup.closure
theorem subgroup.mem_closure {G : Type u_1} [group G] {k : set G} {x : G} :
x subgroup.closure k ∀ (K : subgroup G), k Kx 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 Kx K
@[simp]
theorem subgroup.subset_closure {G : Type u_1} [group G] {k : set G} :

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} :

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 subgroup.closure_le {G : Type u_1} [group G] (K : subgroup G) {k : set G} :

A subgroup K includes closure k if and only if it includes k.

@[simp]
theorem add_subgroup.closure_le {G : Type u_1} [add_group G] (K : add_subgroup G) {k : set G} :

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) :
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 kp x) (H1 : p 1) (Hmul : ∀ (x y : G), p xp yp (x * y)) (Hinv : ∀ (x : G), p xp 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 kp x) (H1 : p 0) (Hmul : ∀ (x y : G), p xp yp (x + y)) (Hinv : ∀ (x : G), p xp (-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 hxp y hyp (x * y) _) (Hinv : ∀ (x : G) (hx : x subgroup.closure k), p x hxp 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 hxp y hyp (x + y) _) (Hinv : ∀ (x : G) (hx : x add_subgroup.closure k), p x hxp (-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 kp x y) (H1_left : ∀ (x : G), p 0 x) (H1_right : ∀ (x : G), p x 0) (Hmul_left : ∀ (x₁ x₂ y : G), p x₁ yp x₂ yp (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 yp (-x) y) (Hinv_right : ∀ (x y : G), p x yp 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 kp x y) (H1_left : ∀ (x : G), p 1 x) (H1_right : ∀ (x : G), p x 1) (Hmul_left : ∀ (x₁ x₂ y : G), p x₁ yp x₂ yp (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 yp x⁻¹ y) (Hinv_right : ∀ (x y : G), p x yp 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} :
def subgroup.closure_comm_group_of_comm {G : Type u_1} [group G] {k : set G} (hcomm : ∀ (x : G), x k∀ (y : G), y kx * y = y * x) :

If all the elements of a set s commute, then closure s is a commutative group.

Equations
@[protected]

closure forms a Galois insertion with the coercion to set.

Equations
@[protected]

closure forms a Galois insertion with the coercion to set.

Equations
theorem subgroup.closure_mono {G : Type u_1} [group G] ⦃h k : set G⦄ (h' : h k) :

Subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k.

theorem add_subgroup.closure_mono {G : Type u_1} [add_group G] ⦃h k : set G⦄ (h' : h k) :

Additive subgroup closure of a set is monotone in its argument: if h ⊆ k, then closure h ≤ closure k

@[simp]
theorem subgroup.closure_eq {G : Type u_1} [group G] (K : subgroup G) :

Closure of a subgroup K equals K.

@[simp]
theorem add_subgroup.closure_eq {G : Type u_1} [add_group G] (K : add_subgroup G) :

Additive closure of an additive subgroup K equals K

@[simp]
@[simp]
theorem subgroup.closure_empty {G : Type u_1} [group G] :
@[simp]
theorem subgroup.closure_univ {G : Type u_1} [group G] :
theorem subgroup.closure_union {G : Type u_1} [group G] (s t : set G) :
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) :
theorem add_subgroup.closure_eq_bot_iff (G : Type u_1) [add_group G] (S : set G) :
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))
theorem add_subgroup.mem_closure_singleton {G : Type u_1} [add_group G] {x y : G} :
y add_subgroup.closure {x} ∃ (n : ), n x = y

The add_subgroup generated by an element of an add_group equals the set of natural number multiples of the element.

theorem subgroup.mem_closure_singleton {G : Type u_1} [group G] {x y : G} :
y subgroup.closure {x} ∃ (n : ), x ^ n = y

The subgroup generated by an element of a group equals the set of integer number powers of the element.

theorem subgroup.closure_singleton_one {G : Type u_1} [group G] :
@[simp]
theorem subgroup.inv_subset_closure {G : Type u_1} [group G] (S : set G) :
@[simp]
theorem add_subgroup.neg_subset_closure {G : Type u_1} [add_group G] (S : set G) :
@[simp]
theorem subgroup.closure_inv {G : Type u_1} [group G] (S : set G) :
@[simp]
theorem add_subgroup.closure_induction_left {G : Type u_1} [add_group G] {k : set G} {p : G → Prop} {x : G} (h : x add_subgroup.closure k) (H1 : p 0) (Hmul : ∀ (x : G), x k∀ (y : G), p yp (x + y)) (Hinv : ∀ (x : G), x k∀ (y : G), p yp (-x + y)) :
p x
theorem subgroup.closure_induction_left {G : Type u_1} [group G] {k : set G} {p : G → Prop} {x : G} (h : x subgroup.closure k) (H1 : p 1) (Hmul : ∀ (x : G), x k∀ (y : G), p yp (x * y)) (Hinv : ∀ (x : G), x k∀ (y : G), p yp (x⁻¹ * y)) :
p x
theorem add_subgroup.closure_induction_right {G : Type u_1} [add_group G] {k : set G} {p : G → Prop} {x : G} (h : x add_subgroup.closure k) (H1 : p 0) (Hmul : ∀ (x y : G), y kp xp (x + y)) (Hinv : ∀ (x y : G), y kp xp (x + -y)) :
p x
theorem subgroup.closure_induction_right {G : Type u_1} [group G] {k : set G} {p : G → Prop} {x : G} (h : x subgroup.closure k) (H1 : p 1) (Hmul : ∀ (x y : G), y kp xp (x * y)) (Hinv : ∀ (x y : G), y kp xp (x * y⁻¹))<