# mathlibdocumentation

group_theory.subgroup

# 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 N` are `group`s

• `A` is an `add_group`

• `H K` are `subgroup`s of `G` or `add_subgroup`s of `A`

• `x` is an element of type `G` or type `A`

• `f g : N →* G` are group homomorphisms

• `s k` are sets of elements of type `G`

Definitions in the file:

• `subgroup G` : the type of subgroups of a group `G`

• `add_subgroup A` : the type of subgroups of an additive group `A`

• `complete_lattice (subgroup G)` : the subgroups of `G` form a complete lattice

• `subgroup.closure k` : the minimal subgroup that includes the set `k`

• `subgroup.subtype` : the natural group homomorphism from a subgroup of group `G` to `G`

• `subgroup.gi` : `closure` forms a Galois insertion with the coercion to set

• `subgroup.comap H f` : the preimage of a subgroup `H` along the group homomorphism `f` is also a subgroup

• `subgroup.map f H` : the image of a subgroup `H` along the group homomorphism `f` is also a subgroup

• `subgroup.prod H K` : the product of subgroups `H`, `K` of groups `G`, `N` respectively, `H × K` is a subgroup of `G × N`

• `monoid_hom.range f` : the range of the group homomorphism `f` is a subgroup

• `monoid_hom.ker f` : the kernel of a group homomorphism `f` is the subgroup of elements `x : G` such that `f x = 1`

• `monoid_hom.eq_locus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that `f x = g x` form a subgroup of `G`

• `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

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.

Type u_3

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

Reinterpret an `add_subgroup` as an `add_submonoid`.

@[protected, instance]
def subgroup.set_like {G : Type u_1} [group G] :
Equations
@[protected, instance]
G
@[simp]
theorem subgroup.mem_carrier {G : Type u_1} [group G] {s : subgroup G} {x : G} :
x s.carrier x s
@[simp]
x s.carrier x s
def subgroup.simps.coe {G : Type u_1} [group G] (S : subgroup G) :
set G
Equations
set G
@[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) :
x K
@[simp]
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
@[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] :
theorem subgroup.to_submonoid_injective {G : Type u_1} [group G] :
@[simp]
p = q
@[simp]
theorem subgroup.to_submonoid_eq {G : Type u_1} [group G] {p q : subgroup G} :
p = q
theorem subgroup.to_submonoid_strict_mono {G : Type u_1} [group G] :
theorem subgroup.to_submonoid_mono {G : Type u_1} [group G] :
@[simp]
p q
@[simp]
theorem subgroup.to_submonoid_le {G : Type u_1} [group G] {p q : subgroup G} :
p q

### Conversion to/from `additive`/`multiplicative`#

def subgroup.to_add_subgroup {G : Type u_1} [group G] :

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

Equations
@[simp]
theorem subgroup.to_add_subgroup_apply_coe {G : Type u_1} [group G] (S : subgroup G) :
@[simp]
def add_subgroup.to_subgroup' {G : Type u_1} [group G] :

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
@[simp]
@[simp]
theorem add_subgroup.to_subgroup_symm_apply_coe {A : Type u_2} [add_group A] (S : subgroup ) :

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

@[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_subgroup`s are equal if they have the same elements.

theorem subgroup.one_mem {G : Type u_1} [group G] (H : subgroup G) :
1 H

A subgroup contains the group's 1.

0 H

An `add_subgroup` contains the group's 0.

x Hy Hx + y H

An `add_subgroup` is closed under addition.

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.

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

A subgroup is closed under inverse.

x H-x H

An `add_subgroup` is closed under inverse.

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.

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.

@[simp]
-x H x H
@[simp]
theorem subgroup.inv_mem_iff {G : Type u_1} [group G] (H : subgroup G) {x : G} :
x⁻¹ H x H
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
theorem subgroup.div_mem_comm_iff {G : Type u_1} [group G] (H : subgroup G) {a b : G} :
a / b H b / a H
@[simp]
@[simp]
theorem subgroup.inv_coe_set {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
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
@[simp]
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
y + x H y H
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
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
x + y H y H
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.

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`.

theorem add_subgroup.multiset_sum_mem {G : Type u_1} (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`.

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 add_subgroup.sum_mem {G : Type u_1} (K : add_subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (h : ∀ (c : ι), c tf c K) :
∑ (c : ι) in 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`.

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) :
∏ (c : ι) in t, f c K

Product of elements of a subgroup of a `comm_group` indexed by a `finset` is in the subgroup.

theorem subgroup.pow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x K) (n : ) :
x ^ n K
theorem subgroup.gpow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x K) (n : ) :
x ^ n K
def subgroup.of_div {G : Type u_1} [group G] (s : set G) (hsn : s.nonempty) (hs : ∀ (x y : G), x sy 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 y : G), x sy sx + -y s) :

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

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

An `add_subgroup` of an `add_group` inherits an addition.

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

An `add_subgroup` of an `add_group` inherits a zero.

@[protected, instance]

A `add_subgroup` of a `add_group` inherits an inverse.

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

An `add_subgroup` of an `add_group` inherits a subtraction.

@[simp, norm_cast]
(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]
0 = 0
@[simp, norm_cast]
theorem subgroup.coe_one {G : Type u_1} [group G] (H : subgroup G) :
1 = 1
@[simp, norm_cast]
@[simp, norm_cast]
theorem subgroup.coe_inv {G : Type u_1} [group G] (H : subgroup G) (x : H) :
@[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
@[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]

An `add_subgroup` of an `add_group` inherits an `add_group` structure.

@[protected, instance]

An `add_subgroup` of an `add_comm_group` is an `add_comm_group`.

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

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

A subgroup of an `ordered_comm_group` is an `ordered_comm_group`.

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

A subgroup of a `linear_ordered_comm_group` is a `linear_ordered_comm_group`.

Equations
@[protected, instance]

An `add_subgroup` of a `linear_ordered_add_comm_group` is a `linear_ordered_add_comm_group`.

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

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

@[simp]
theorem subgroup.coe_subtype {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
@[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 subgroup.coe_gpow {G : Type u_1} [group G] (H : subgroup G) (x : H) (n : ) :
(x ^ n) = x ^ n
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`.

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) :
( a) = a
@[simp]
theorem add_subgroup.coe_inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} {h : H K} (a : H) :
a) = a
@[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]

The `add_subgroup G` of the `add_group G`.

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

The subgroup `G` of the group `G`.

Equations
@[protected, instance]

The trivial `add_subgroup` `{0}` of an `add_group` `G`.

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

The trivial subgroup `{1}` of an group `G`.

Equations
@[protected, instance]
@[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]
@[simp]
= {0}
@[simp]
theorem subgroup.coe_bot {G : Type u_1} [group G] :
= {1}
theorem subgroup.eq_bot_iff_forall {G : Type u_1} [group G] (H : subgroup G) :
H = ∀ (x : G), x Hx = 1
H = ∀ (x : G), x Hx = 0
theorem subgroup.eq_bot_of_subsingleton {G : Type u_1} [group G] (H : subgroup G)  :
H =
H =
@[protected, instance]
def subgroup.fintype_bot {G : Type u_1} [group G] :
Equations
@[protected, instance]
@[simp]
@[simp]
theorem subgroup.card_bot {G : Type u_1} [group G] :
theorem subgroup.eq_top_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype H] [fintype G] (h : = ) :
H =
theorem add_subgroup.eq_top_of_card_eq {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype H] [fintype G] (h : = ) :
H =
∃ (x : G) (H : x H), x 0
theorem subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [group G] (H : subgroup G) :
∃ (x : G) (H : x H), x 1
theorem subgroup.bot_or_nontrivial {G : Type u_1} [group G] (H : subgroup G) :
H =

A subgroup is either the trivial subgroup or nontrivial.

H =
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 nonzero element.

H = ∃ (x : G) (H : x H), x 0
@[protected, instance]
def subgroup.has_inf {G : Type u_1} [group G] :

The inf of two subgroups is their intersection.

Equations
@[protected, instance]

The inf of two `add_subgroups`s is their intersection.

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

Subgroups of a group form a complete lattice.

Equations
@[protected, instance]

The `add_subgroup`s of an `add_group` form a complete lattice.

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.mem_supr_of_mem {G : Type u_1} [group G] {ι : Type u_2} {S : ι → } (i : ι) {x : G} :
x S ix supr S
theorem add_subgroup.mem_supr_of_mem {G : Type u_1} [add_group G] {ι : Type u_2} {S : ι → } (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 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 Sup S
theorem subgroup.subsingleton_iff {G : Type u_1} [group G] :
theorem subgroup.nontrivial_iff {G : Type u_1} [group G] :
@[protected, instance]
@[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]
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

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

The `subgroup` generated by a set.

Equations
theorem subgroup.mem_closure {G : Type u_1} [group G] {k : set G} {x : G} :
∀ (K : subgroup G), k Kx K
theorem add_subgroup.mem_closure {G : Type u_1} [add_group G] {k : set G} {x : G} :
∀ (K : , k Kx K
@[simp]
theorem subgroup.subset_closure {G : Type u_1} [group G] {k : set G} :
k

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.

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

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} :
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 ) :
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 ) :
theorem subgroup.closure_induction {G : Type u_1} [group G] {k : set G} {p : G → Prop} {x : G} (h : x ) (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 ) (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 : → Prop} (Hk : ∀ (x : G) (h : x k), p x, _⟩) (H1 : p 1) (Hmul : ∀ (x y : (subgroup.closure k)), p xp yp (x * y)) (Hinv : ∀ (x : (subgroup.closure k)), p xp x⁻¹) (x : ) :
p x

An induction principle on elements of the subtype `subgroup.closure`. If `p` holds for `1` and all elements of `k`, and is preserved under multiplication and inverse, then `p` holds for all elements `x : closure k`.

The difference with `subgroup.closure_induction` is that this acts on the subtype.

theorem add_subgroup.closure_induction' {G : Type u_1} [add_group G] (k : set G) {p : → Prop} (Hk : ∀ (x : G) (h : x k), p x, _⟩) (H1 : p 0) (Hmul : ∀ (x y : , p xp yp (x + y)) (Hinv : ∀ (x : , p xp (-x)) (x : ) :
p x

An induction principle on elements of the subtype `add_subgroup.closure`. If `p` holds for `0` and all elements of `k`, and is preserved under addition and negation, then `p` holds for all elements `x : closure k`.

The difference with `add_subgroup.closure_induction` is that this acts on the subtype.

@[protected]

`closure` forms a Galois insertion with the coercion to set.

@[protected]
def subgroup.gi (G : Type u_1) [group G] :

`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]

Additive closure of an additive subgroup `K` equals `K`

@[simp]
@[simp]
theorem subgroup.closure_empty {G : Type u_1} [group G] :
@[simp]
@[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 add_subgroup.closure_union {G : Type u_1} [add_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) :
S {1}
theorem add_subgroup.closure_eq_bot_iff (G : Type u_1) [add_group G] (S : set G) :
S {0}
theorem subgroup.mem_closure_singleton {G : Type u_1} [group G] {x y : G} :
y ∃ (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_neg {G : Type u_1} [add_group G] (S : set G) :
theorem subgroup.closure_to_submonoid {G : Type u_1} [group G] (S : set G) :
theorem subgroup.closure_induction'' {G : Type u_1} [group G] {k : set G} {p : G → Prop} {x : G} (h : x ) (Hk : ∀ (x : G), x kp x) (Hk_inv : ∀ (x : G), x kp x⁻¹) (H1 : p 1) (Hmul : ∀ (x y : G), p xp yp (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 ) (Hk : ∀ (x : G), x kp x) (Hk_inv : ∀ (x : G), x kp (-x)) (H1 : p 0) (Hmul : ∀ (x y : G), p xp yp (x + y)) :
p x

An induction principle for additive closure membership. If `p` holds for `0` and all elements of `k` and their negation, and is preserved under addition, then `p` holds for all elements of the additive closure of `k`.

theorem add_subgroup.mem_supr_of_directed {G : Type u_1} [add_group G] {ι : Sort u_2} [hι : nonempty ι] {K : ι → } (hK : K) {x : G} :
x supr K ∃ (i : ι), x K i
theorem subgroup.mem_supr_of_directed {G : Type u_1} [group G] {ι : Sort u_2} [hι : nonempty ι] {K : ι → } (hK : K) {x : G} :
x supr K ∃ (i : ι), x K i
theorem subgroup.coe_supr_of_directed {G : Type u_1} [group G] {ι : Sort u_2} [nonempty ι] {S : ι → } (hS : S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem add_subgroup.coe_supr_of_directed {G : Type u_1} [add_group G] {ι : Sort u_2} [nonempty ι] {S : ι → } (hS : S) :
(⨆ (i : ι), S i) = ⋃ (i : ι), (S i)
theorem add_subgroup.mem_Sup_of_directed_on {G : Type u_1} [add_group G] {K : set (add_subgroup G)} (Kne : K.nonempty) (hK : K) {x : G} :
x Sup K ∃ (s : (H : s K), x s
theorem subgroup.mem_Sup_of_directed_on {G : Type u_1} [group G] {K : set (subgroup G)} (Kne : K.nonempty) (hK : K) {x : G} :
x Sup K ∃ (s : subgroup G) (H : s K), x s
def subgroup.comap {G : Type u_1} [group G] {N : Type u_2} [group N] (f : G →* N) (H : subgroup N) :

The preimage of a subgroup along a monoid homomorphism is a subgroup.

Equations
def add_subgroup.comap {G : Type u_1} [add_group G] {N : Type u_2} [add_group N] (f : G →+ N) (H : add_subgroup N) :

The preimage of an `add_subgroup` along an `add_monoid` homomorphism is an `add_subgroup`.

@[simp]
theorem subgroup.coe_comap {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup N) (f : G →* N) :
@[simp]
theorem add_subgroup.coe_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (K : add_subgroup N) (f : G →+ N) :
@[simp]
theorem add_subgroup.mem_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {K : add_subgroup N} {f : G →+ N} {x : G} :
x f x K
@[simp]
theorem subgroup.mem_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {K : subgroup N} {f : G →* N} {x : G} :
x f x K
theorem subgroup.comap_mono {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K K' : subgroup N} :
K K' K'
theorem add_subgroup.comap_mono {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K K' : add_subgroup N} :
K K'
theorem add_subgroup.comap_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {P : Type u_4} [add_group P] (K : add_subgroup P) (g : N →+ P) (f : G →+ N) :
theorem subgroup.comap_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {P : Type u_4} [group P] (K : subgroup P) (g : N →* P) (f : G →* N) :
K) = subgroup.comap (g.comp f) K
def add_subgroup.map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (H : add_subgroup G) :

The image of an `add_subgroup` along an `add_monoid` homomorphism is an `add_subgroup`.

def subgroup.map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (H : subgroup G) :

The image of a subgroup along a monoid homomorphism is a subgroup.

Equations
@[simp]
theorem add_subgroup.coe_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (K : add_subgroup G) :
K) = f '' K
@[simp]
theorem subgroup.coe_map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (K : subgroup G) :
K) = f '' K
@[simp]
theorem add_subgroup.mem_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K : add_subgroup G} {y : N} :
y ∃ (x : G) (H : x K), f x = y
@[simp]
theorem subgroup.mem_map {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K : subgroup G} {y : N} :
y K ∃ (x : G) (H : x K), f x = y
theorem add_subgroup.mem_map_of_mem {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) {K : add_subgroup G} {x : G} (hx : x K) :
f x
theorem subgroup.mem_map_of_mem {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) {K : subgroup G} {x : G} (hx : x K) :
f x K
theorem add_subgroup.apply_coe_mem_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) {K : add_subgroup G} (x : K) :
theorem subgroup.apply_coe_mem_map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) {K : subgroup G} (x : K) :
f x K
theorem add_subgroup.map_mono {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K K' : add_subgroup G} :
K K' K'
theorem subgroup.map_mono {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K K' : subgroup G} :
K K' K K'
theorem add_subgroup.map_map {G : Type u_1} [add_group G] (K : add_subgroup G) {N : Type u_3} [add_group N] {P : Type u_4} [add_group P] (g : N →+ P) (f : G →+ N) :
K) = add_subgroup.map (g.comp f) K
theorem subgroup.map_map {G : Type u_1} [group G] (K : subgroup G) {N : Type u_3} [group N] {P : Type u_4} [group P] (g : N →* P) (f : G →* N) :
K) = subgroup.map (g.comp f) K
theorem add_subgroup.map_le_iff_le_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K : add_subgroup G} {H : add_subgroup N} :
H K
theorem subgroup.map_le_iff_le_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K : subgroup G} {H : subgroup N} :
K H K
theorem subgroup.gc_map_comap {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
theorem add_subgroup.gc_map_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
theorem add_subgroup.map_sup {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup G) (f : G →+ N) :
(H K) =
theorem subgroup.map_sup {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup G) (f : G →* N) :
(H K) = H K
theorem add_subgroup.map_supr {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι → ) :
(supr s) = ⨆ (i : ι), (s i)
theorem subgroup.map_supr {G : Type u_1} [group G] {N : Type u_3} [group N] {ι : Sort u_2} (f : G →* N) (s : ι → ) :
(supr s) = ⨆ (i : ι), (s i)
theorem add_subgroup.comap_inf {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup N) (f : G →+ N) :
(H K) =
theorem subgroup.comap_inf {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup N) (f : G →* N) :
(H K) =
theorem subgroup.comap_infi {G : Type u_1} [group G] {N : Type u_3} [group N] {ι : Sort u_2} (f : G →* N) (s : ι → ) :
(infi s) = ⨅ (i : ι), (s i)
theorem add_subgroup.comap_infi {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι → ) :
(infi s) = ⨅ (i : ι), (s i)
@[simp]
theorem add_subgroup.map_bot {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
@[simp]
theorem subgroup.map_bot {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
@[simp]
theorem subgroup.comap_top {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
@[simp]
theorem add_subgroup.comap_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
@[simp]
(H K) =
@[simp]
theorem subgroup.comap_subtype_inf_left {G : Type u_1} [group G] {H K : subgroup G} :
(H K) =
@[simp]
(H K) =
@[simp]
theorem subgroup.comap_subtype_inf_right {G : Type u_1} [group G] {H K : subgroup G} :
(H K) =

Given `add_subgroup`s `H`, `K` of `add_group`s `A`, `B` respectively, `H × K` as an `add_subgroup` of `A × B`.

def subgroup.prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) :
subgroup (G × N)

Given `subgroup`s `H`, `K` of groups `G`, `N` respectively, `H × K` as a subgroup of `G × N`.

Equations
theorem subgroup.coe_prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) :
(H.prod K) = H.prod K
(H.prod K) = H.prod K
theorem add_subgroup.mem_prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {H : add_subgroup G} {K : add_subgroup N} {p : G × N} :
p H.prod K p.fst H p.snd K
theorem subgroup.mem_prod {G : Type u_1} [group G] {N : Type u_3} [group N] {H : subgroup G} {K : subgroup N} {p : G × N} :
p H.prod K p.fst H p.snd K
theorem subgroup.prod_mono {G : Type u_1} [group G] {N : Type u_3} [group N] :
theorem subgroup.prod_mono_right {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup G) :
monotone (λ (t : subgroup N), K.prod t)
monotone (λ (t : , K.prod t)
monotone (λ (K : , K.prod H)
theorem subgroup.prod_mono_left {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup N) :
monotone (λ (K : subgroup G), K.prod H)
theorem subgroup.prod_top {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup G) :
K.prod = K
theorem subgroup.top_prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup N) :
.prod H = H
@[simp]
theorem subgroup.top_prod_top {G : Type u_1} [group G] {N : Type u_3} [group N] :
@[simp]
theorem subgroup.bot_prod_bot {G : Type u_1} [group G] {N : Type u_3} [group N] :
def subgroup.prod_equiv {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) :

Product of subgroups is isomorphic to their product as groups.

Equations

Product of additive subgroups is isomorphic to their product as additive groups

@[class]
structure subgroup.normal {G : Type u_1} [group G] (H : subgroup G) :
Prop
• conj_mem : ∀ (n : G), n H∀ (g : G), (g * n) * g⁻¹ H

A subgroup is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G`

Instances
@[class]
Prop
• conj_mem : ∀ (n : A), n H∀ (g : A), g + n + -g H

An add_subgroup is normal if whenever `n ∈ H`, then `g + n - g ∈ H` for every `g : G`

Instances
@[protected, instance]
def subgroup.normal_of_comm {G : Type u_1} [comm_group G] (H : subgroup G) :
@[protected, instance]
theorem add_subgroup.normal.mem_comm {G : Type u_1} [add_group G] {H : add_subgroup G} (nH : H.normal) {a b : G} (h : a + b H) :
b + a H
theorem subgroup.normal.mem_comm {G : Type u_1} [group G] {H : subgroup G} (nH : H.normal) {a b : G} (h : a * b H) :
b * a H
theorem subgroup.normal.mem_comm_iff {G : Type u_1} [group G] {H : subgroup G} (nH : H.normal) {a b : G} :
a * b H b * a H
theorem add_subgroup.normal.mem_comm_iff {G : Type u_1} [add_group G] {H : add_subgroup G} (nH : H.normal) {a b : G} :
a + b H b + a H
@[protected, instance]
@[protected, instance]
def subgroup.bot_normal {G : Type u_1} [group G] :
@[protected, instance]
def subgroup.top_normal {G : Type u_1} [group G] :
@[protected, instance]

The center of a group `G` is the set of elements that commute with everything in `G`

def subgroup.center (G : Type u_1) [group G] :

The center of a group `G` is the set of elements that commute with everything in `G`

Equations
theorem subgroup.mem_center_iff {G : Type u_1} [group G] {z : G} :
∀ (g : G), g * z = z * g
theorem add_subgroup.mem_center_iff {G : Type u_1} [add_group G] {z : G} :
∀ (g : G), g + z = z + g
@[protected, instance]
@[protected, instance]
def subgroup.center_normal {G : Type u_1} [group G] :

The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal.

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

The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal.

Equations
def subgroup.set_normalizer {G : Type u_1} [group G] (S : set G) :

The `set_normalizer` of `S` is the subgroup of `G` whose elements satisfy `g*S*g⁻¹=S`

Equations
def add_subgroup.set_normalizer {G : Type u_1} [add_group G] (S : set G) :

The `set_normalizer` of `S` is the subgroup of `G` whose elements satisfy `g+S-g=S`.

theorem subgroup.mem_normalizer_fintype {G : Type u_1} [group G] {S : set G} [fintype S] {x : G} (h : ∀ (n : G), n S(x * n) * x⁻¹ S) :
g H.normalizer ∀ (n : G), n H g + n + -g H
theorem subgroup.mem_normalizer_iff {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g H.normalizer ∀ (n : G), n H (g * n) * g⁻¹ H
theorem subgroup.le_normalizer {G : Type u_1} [group G] {H : subgroup G} :
@[protected, instance]
@[protected, instance]
def subgroup.normal_in_normalizer {G : Type u_1} [group G] {H : subgroup G} :
theorem subgroup.le_normalizer_of_normal {G : Type u_1} [group G] {H K : subgroup G} [hK : H).normal] (HK : H K) :
theorem add_subgroup.le_normalizer_of_normal {G : Type u_1} [add_group G] {H K : add_subgroup G} [hK : .normal] (HK : H K) :
def group.conjugates_of_set {G : Type u_1} [group G] (s : set G) :
set G

Given a set `s`, `conjugates_of_set s` is the set of all conjugates of the elements of `s`.

Equations
• = ⋃ (a : G) (H : a s),
theorem group.mem_conjugates_of_set_iff {G : Type u_1} [group G] {s : set G} {x : G} :
∃ (a : G) (H : a s), x
theorem group.subset_conjugates_of_set {G : Type u_1} [group G] {s : set G} :
theorem group.conjugates_of_set_mono {G : Type u_1} [group G] {s t : set G} (h : s t) :
theorem group.conjugates_subset_normal {G : Type u_1} [group G] {N : subgroup G} [tn : N.normal] {a : G} (h : a N) :
theorem group.conjugates_of_set_subset {G : Type u_1} [group G] {s : set G} {N : subgroup G} [N.normal] (h : s N) :
theorem group.conj_mem_conjugates_of_set {G : Type u_1} [group G] {s : set G} {x c : G} :
(c * x) * c⁻¹

The set of conjugates of `s` is closed under conjugation.

def subgroup.normal_closure {G : Type u_1} [group G] (s : set G) :

The normal closure of a set `s` is the subgroup closure of all the conjugates of elements of `s`. It is the smallest normal subgroup containing `s`.

Equations
theorem subgroup.conjugates_of_set_subset_normal_closure {G : Type u_1} [group G] {s : set G} :
theorem subgroup.subset_normal_closure {G : Type u_1} [group G] {s : set G} :
theorem subgroup.le_normal_closure {G : Type u_1} [group G] {H : subgroup G} :
@[protected, instance]
def subgroup.normal_closure_normal {G : Type u_1} [group G] {s : set G} :

The normal closure of `s` is a normal subgroup.

theorem subgroup.normal_closure_le_normal {G : Type u_1} [group G] {s : set G} {N : subgroup G} [N.normal] (h : s N) :

The normal closure of `s` is the smallest normal subgroup containing `s`.

theorem subgroup.normal_closure_subset_iff {G : Type u_1} [group G] {s : set G} {N : subgroup G} [N.normal] :
s N
theorem subgroup.normal_closure_mono {G : Type u_1} [group G] {s t : set G} (h : s t) :
theorem subgroup.normal_closure_eq_infi {G : Type u_1} [group G] {s : set G} :
= ⨅ (N : subgroup G) [_inst_3 : N.normal] (hs : s N), N
@[simp]
theorem subgroup.normal_closure_eq_self {G : Type u_1} [group G] (H : subgroup G) [H.normal] :
@[simp]
theorem subgroup.normal_closure_idempotent {G : Type u_1} [group G] {s : set G} :
theorem subgroup.closure_le_normal_closure {G : Type u_1} [group G] {s : set G} :
@[simp]
theorem subgroup.normal_closure_closure_eq_normal_closure {G : Type u_1} [group G] {s : set G} :
theorem add_subgroup.gsmul_mem {A : Type u_2} [add_group A] (H : add_subgroup A) {x : A} (hx : x H) (n : ) :
n x H
theorem add_subgroup.mem_closure_singleton {A : Type u_2} [add_group A] {x y : A} :
∃ (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.

@[simp]
theorem add_subgroup.coe_smul {A : Type u_2} [add_group A] (H : add_subgroup A) (x : H) (n : ) :
(n x) = n x
@[simp]
theorem add_subgroup.coe_gsmul {A : Type u_2} [add_group A] (H : add_subgroup A) (x : H) (n : ) :
(n x) = n x
def add_monoid_hom.range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

The range of an `add_monoid_hom` from an `add_group` is an `add_subgroup`.

def monoid_hom.range {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

The range of a monoid homomorphism from a group is a subgroup.

Equations
@[protected, instance]
def add_monoid_hom.decidable_mem_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) [fintype G] [decidable_eq N] :
decidable_pred (λ (x : N), x f.range)
@[protected, instance]
def monoid_hom.decidable_mem_range {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) [fintype G] [decidable_eq N] :
decidable_pred (λ (x : N), x f.range)
Equations
@[simp]
theorem add_monoid_hom.coe_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
(f.range) =
@[simp]
theorem monoid_hom.coe_range {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
(f.range) =
@[simp]
theorem monoid_hom.mem_range {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {y : N} :
y f.range ∃ (x : G), f x = y
@[simp]
theorem add_monoid_hom.mem_range {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {y : N} :
y f.range ∃ (x : G), f x = y
theorem monoid_hom.range_eq_map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
f.range =
theorem add_monoid_hom.range_eq_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
def monoid_hom.range_restrict {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

The canonical surjective group homomorphism `G →* f(G)` induced by a group homomorphism `G →* N`.

Equations
def add_monoid_hom.range_restrict {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

The canonical surjective `add_group` homomorphism `G →+ f(G)` induced by a group homomorphism `G →+ N`.

@[simp]
theorem monoid_hom.coe_range_restrict {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (g : G) :
@[simp]
theorem add_monoid_hom.coe_range_restrict {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (g : G) :
theorem monoid_hom.map_range {G : Type u_1} [group G] {N : Type u_3} {P : Type u_4} [group N] [group P] (g : N →* P) (f : G →* N) :
= (g.comp f).range
theorem add_monoid_hom.map_range {G : Type u_1} [add_group G] {N : Type u_3} {P : Type u_4} [add_group N] [add_group P] (g : N →+ P) (f : G →+ N) :
= (g.comp f).range
theorem monoid_hom.range_top_iff_surjective {G : Type u_1} [group G] {N : Type u_2} [group N] {f : G →* N} :
theorem add_monoid_hom.range_top_iff_surjective {G : Type u_1} [add_group G] {N : Type u_2} [add_group N] {f : G →+ N} :
theorem monoid_hom.range_top_of_surjective {G : Type u_1} [group G] {N : Type u_2} [group N] (f : G →* N) (hf : function.surjective f) :

The range of a surjective monoid homomorphism is the whole of the codomain.

theorem add_monoid_hom.range_top_of_surjective {G : Type u_1} [add_group G] {N : Type u_2} [add_group N] (f : G →+ N) (hf : function.surjective f) :

The range of a surjective `add_monoid` homomorphism is the whole of the codomain.

@[simp]
@[simp]
theorem subgroup.subtype_range {G : Type u_1} [group G] (H : subgroup G) :
def add_monoid_hom.restrict {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (H : add_subgroup G) :

Restriction of an `add_group` hom to an `add_subgroup` of the domain.

def monoid_hom.restrict {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (H : subgroup G) :

Restriction of a group hom to a subgroup of the domain.

Equations
@[simp]
theorem add_monoid_hom.restrict_apply {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {H : add_subgroup G} (f : G →+ N) (x : H) :
(f.restrict H) x = f x
@[simp]
theorem monoid_hom.restrict_apply {G : Type u_1} [group G] {N : Type u_3} [group N] {H : subgroup G} (f : G →* N) (x : H) :
(f.restrict H) x = f x
def add_monoid_hom.cod_restrict {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (S : add_subgroup N) (h : ∀ (x : G), f x S) :

Restriction of an `add_group` hom to an `add_subgroup` of the codomain.

def monoid_hom.cod_restrict {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (S : subgroup N) (h : ∀ (x : G), f x S) :

Restriction of a group hom to a subgroup of the codomain.

Equations
def monoid_hom.of_left_inverse {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {g : N →* G} (h : f) :

Computable alternative to `monoid_hom.of_injective`.

Equations
@[simp]
theorem monoid_hom.of_left_inverse_apply {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {g : N →* G} (h : f) (x : G) :
x) = f x
@[simp]
theorem monoid_hom.of_left_inverse_symm_apply {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {g : N →* G} (h : f) (x : (f.range)) :
x = g x
def monoid_hom.of_injective {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} (hf : function.injective f) :

The range of an injective group homomorphism is isomorphic to its domain.

Equations
theorem monoid_hom.of_injective_apply {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} (hf : function.injective f) {x : G} :
( x) = f x
def monoid_hom.ker {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :

The multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that `f x = 1`

Equations
def add_monoid_hom.ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :

The additive kernel of an `add_monoid` homomorphism is the `add_subgroup` of elements such that `f x = 0`

theorem monoid_hom.mem_ker {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) {x : G} :
x f.ker f x = 1
theorem add_monoid_hom.mem_ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) {x : G} :
x f.ker f x = 0
theorem add_monoid_hom.coe_ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
(f.ker) = f ⁻¹' {0}
theorem monoid_hom.coe_ker {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
(f.ker) = f ⁻¹' {1}
theorem add_monoid_hom.eq_iff {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) {x y : G} :
f x = f y -y + x f.ker
theorem monoid_hom.eq_iff {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) {x y : G} :
f x = f y y⁻¹ * x f.ker
@[protected, instance]
def monoid_hom.decidable_mem_ker {G : Type u_1} [group G] {N : Type u_3} [group N] [decidable_eq N] (f : G →* N) :
decidable_pred (λ (_x : G), _x f.ker)
Equations
@[protected, instance]
def add_monoid_hom.decidable_mem_ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] [decidable_eq N] (f : G →+ N) :
decidable_pred (λ (_x : G), _x f.ker)
theorem add_monoid_hom.comap_ker {G : Type u_1} [add_group G] {N : Type u_3} {P : Type u_4} [add_group N] [add_group P] (g : N →+ P) (f : G →+ N) :
= (g.comp f).ker
theorem monoid_hom.comap_ker {G : Type u_1} [group G] {N : Type u_3} {P : Type u_4} [group N] [group P] (g : N →* P) (f : G →* N) :
= (g.comp f).ker
theorem add_monoid_hom.range_restrict_ker {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
theorem monoid_hom.range_restrict_ker {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
@[simp]
theorem monoid_hom.ker_one {G : Type u_1} [group G] {N : Type u_3} [group N] :
@[simp]
theorem monoid_hom.ker_eq_bot_iff {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
theorem add_monoid_hom.ker_eq_bot_iff {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
def monoid_hom.eq_locus {G : Type u_1} [group G] {N : Type u_3} [group N] (f g : G →* N) :

The subgroup of elements `x : G` such that `f x = g x`

Equations
def add_monoid_hom.eq_locus {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f g : G →+ N) :

The additive subgroup of elements `x : G` such that `f x = g x`

theorem add_monoid_hom.eq_on_closure {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f g : G →+ N} {s : set G} (h : g s) :
g
theorem monoid_hom.eq_on_closure {G : Type u_1} [group G] {N : Type u_3} [group N] {f g : G →* N} {s : set G} (h : g s) :
g

If two monoid homomorphisms are equal on a set, then they are equal on its subgroup closure.

theorem add_monoid_hom.eq_of_eq_on_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f g : G →+ N} (h : g ) :
f = g
theorem monoid_hom.eq_of_eq_on_top {G : Type u_1} [group G] {N : Type u_3} [group N] {f g : G →* N} (h : g ) :
f = g
theorem add_monoid_hom.eq_of_eq_on_dense {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {s : set G} (hs : = ) {f g : G →+ N} (h : g s) :
f = g
theorem monoid_hom.eq_of_eq_on_dense {G : Type u_1} [group G] {N : Type u_3} [group N] {s : set G} (hs : = ) {f g : G →* N} (h : g s) :
f = g
theorem monoid_hom.gclosure_preimage_le {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (s : set N) :
theorem add_monoid_hom.gclosure_preimage_le {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (s : set N) :
theorem add_monoid_hom.map_closure {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (s : set G) :

The image under an `add_monoid` hom of the `add_subgroup` generated by a set equals the `add_subgroup` generated by the image of the set.

theorem monoid_hom.map_closure {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (s : set G) :

The image under a monoid homomorphism of the subgroup generated by a set equals the subgroup generated by the image of the set.

theorem subgroup.map_eq_bot_iff {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) {f : G →* N} :
H = H f.ker
theorem add_subgroup.map_eq_bot_iff {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup G) {f : G →+ N} :
H f.ker
theorem subgroup.map_eq_bot_iff_of_injective {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) {f : G →* N} (hf : function.injective f) :
H = H =
theorem add_subgroup.map_eq_bot_iff_of_injective {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup G) {f : G →+ N} (hf : function.injective f) :
H =
theorem add_subgroup.map_le_range {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] (f : G →+ H) (K : add_subgroup G) :
theorem subgroup.map_le_range {G : Type u_1} [group G] {H : Type u_3} [group H] (f : G →* H) (K : subgroup G) :
K f.range
theorem subgroup.ker_le_comap {G : Type u_1} [group G] {H : Type u_3} [group H] (f : G →* H) (K : subgroup H) :
f.ker
theorem add_subgroup.ker_le_comap {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] (f : G →+ H) (K : add_subgroup H) :
f.ker
theorem add_subgroup.map_comap_le {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] (f : G →+ H) (K : add_subgroup H) :
K
theorem subgroup.map_comap_le {G : Type u_1} [group G] {H : Type u_3} [group H] (f : G →* H) (K : subgroup H) :
K) K
theorem subgroup.le_comap_map {G : Type u_1} [group G] {H : Type u_3} [group H] (f : G →* H) (K : subgroup G) :
K K)
theorem add_subgroup.le_comap_map {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] (f : G →+ H) (K : add_subgroup G) :
K
theorem add_subgroup.map_comap_eq {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] (f : G →+ H) (K : add_subgroup H) :
= f.range K
theorem subgroup.map_comap_eq {G : Type u_1} [group G] {H : Type u_3} [group H] (f : G →* H) (K : subgroup H) :
K) = f.range K
theorem add_subgroup.comap_map_eq {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] (f : G →+ H) (K : add_subgroup G) :
= K f.ker
theorem subgroup.comap_map_eq {G : Type u_1} [group G] {H : Type u_3} [group H] (f : G →* H) (K : subgroup G) :
K) = K f.ker
theorem add_subgroup.map_comap_eq_self {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] {f : G →+ H} {K : add_subgroup H} (h : K f.range) :
= K
theorem subgroup.map_comap_eq_self {G : Type u_1} [group G] {H : Type u_3} [group H] {f : G →* H} {K : subgroup H} (h : K f.range) :
K) = K
theorem add_subgroup.map_comap_eq_self_of_surjective {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] {f : G →+ H} (h : function.surjective f) (K : add_subgroup H) :
= K
theorem subgroup.map_comap_eq_self_of_surjective {G : Type u_1} [group G] {H : Type u_3} [group H] {f : G →* H} (h : function.surjective f) (K : subgroup H) :
K) = K
theorem subgroup.comap_injective {G : Type u_1} [group G] {H : Type u_3} [group H] {f : G →* H} (h : function.surjective f) :
theorem add_subgroup.comap_injective {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] {f : G →+ H} (h : function.surjective f) :
theorem subgroup.comap_map_eq_self {G : Type u_1} [group G] {H : Type u_3} [group H] {f : G →* H} {K : subgroup G} (h : f.ker K) :
K) = K
theorem add_subgroup.comap_map_eq_self {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] {f : G →+ H} {K : add_subgroup G} (h : f.ker K) :
= K
theorem subgroup.comap_map_eq_self_of_injective {G : Type u_1} [group G] {H : Type u_3} [group H] {f : G →* H} (h : function.injective f) (K : subgroup G) :
K) = K
theorem add_subgroup.comap_map_eq_self_of_injective {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] {f : G →+ H} (h : function.injective f) (K : add_subgroup G) :
= K
theorem add_subgroup.map_injective {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] {f : G →+ H} (h : function.injective f) :
theorem subgroup.map_injective {G : Type u_1} [group G] {H : Type u_3} [group H] {f : G →* H} (h : function.injective f) :
theorem subgroup.map_eq_comap_of_inverse {G : Type u_1} [group G] {H : Type u_3} [group H] {f : G →* H} {g : H →* G} (hl : f) (hr : f) (K : subgroup G) :
K =
theorem add_subgroup.map_eq_comap_of_inverse {G : Type u_1} [add_group G] {H : Type u_3} [add_group H] {f : G →+ H} {g : H →+ G} (hl : f) (hr : f) (K : add_subgroup G) :
def add_monoid_hom.lift_of_right_inverse_aux {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : f) (g : G₁ →+ G₃) (hg : f.ker g.ker) :
G₂ →+ G₃

Auxiliary definition used to define `lift_of_right_inverse`

def monoid_hom.lift_of_right_inverse_aux {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : f) (g : G₁ →* G₃) (hg : f.ker g.ker) :
G₂ →* G₃

Auxiliary definition used to define `lift_of_right_inverse`

Equations
@[simp]
theorem monoid_hom.lift_of_right_inverse_aux_comp_apply {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : f) (g : G₁ →* G₃) (hg : f.ker g.ker) (x : G₁) :
(f.lift_of_right_inverse_aux f_inv hf g hg) (f x) = g x
@[simp]
theorem add_monoid_hom.lift_of_right_inverse_aux_comp_apply {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : f) (g : G₁ →+ G₃) (hg : f.ker g.ker) (x : G₁) :
(f.lift_of_right_inverse_aux f_inv hf g hg) (f x) = g x
def add_monoid_hom.lift_of_right_inverse {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ → G₁) (hf : f) :
{g // f.ker g.ker} (G₂ →+ G₃)

`lift_of_right_inverse f f_inv hf g hg` is the unique additive group homomorphism `φ`

• such that `φ.comp f = g` (`add_monoid_hom.lift_of_right_inverse_comp`),
• where `f : G₁ →+ G₂` has a right_inverse `f_inv` (`hf`),
• and `g : G₂ →+ G₃` satisfies `hg : f.ker ≤ g.ker`.

See `add_monoid_hom.eq_lift_of_right_inverse` for the uniqueness lemma.

``````   G₁.
|  \
f |   \ g
|    \
v     \⌟
G₂----> G₃
∃!φ
``````
def monoid_hom.lift_of_right_inverse {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : f) :
{g // f.ker g.ker} (G₂ →* G₃)

`lift_of_right_inverse f hf g hg` is the unique group homomorphism `φ`

• such that `φ.comp f = g` (`monoid_hom.lift_of_right_inverse_comp`),
• where `f : G₁ →+* G₂` has a right_inverse `f_inv` (`hf`),
• and `g : G₂ →+* G₃` satisfies `hg : f.ker ≤ g.ker`.

See `monoid_hom.eq_lift_of_right_inverse` for the uniqueness lemma.

``````   G₁.
|  \
f |   \ g
|    \
v     \⌟
G₂----> G₃
∃!φ
``````
Equations
@[simp]
def add_monoid_hom.lift_of_surjective {G₁ : Type u_3} {G₂ : Type u_4} {G₃ : Type u_5} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (hf : function.surjective f) :
{g // f.ker g.ker} (G₂ →+ G₃)

A non-computable version of `add_monoid_hom.lift_of_right_inverse` for when no computable right inverse is available.