# mathlib3documentation

group_theory.subgroup.basic

# Subgroups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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`

## 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_4) (G : Type u_5) [has_inv G] [ G] :
Prop

`inv_mem_class S G` states `S` is a type of subsets `s ⊆ G` closed under inverses.

Instances of this typeclass
@[class]
structure neg_mem_class (S : Type u_4) (G : Type u_5) [has_neg G] [ G] :
Prop

`neg_mem_class S G` states `S` is a type of subsets `s ⊆ G` closed under negation.

Instances of this typeclass
@[class]
structure subgroup_class (S : Type u_4) (G : Type u_5) [ G] :
Prop
• to_submonoid_class :
• to_inv_mem_class :

`subgroup_class S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`.

Instances of this typeclass
@[class]
structure add_subgroup_class (S : Type u_4) (G : Type u_5) [ G] :
Prop
• to_neg_mem_class :

`add_subgroup_class S G` states `S` is a type of subsets `s ⊆ G` that are additive subgroups of `G`.

Instances of this typeclass
@[simp]
theorem neg_mem_iff {S : Type u_1} {G : Type u_2} [ G] [ G] {H : S} {x : G} :
-x H x H
@[simp]
theorem inv_mem_iff {S : Type u_1} {G : Type u_2} [ G] [ G] {H : S} {x : G} :
x⁻¹ H x H
theorem div_mem {M : Type u_4} {S : Type u_5} [ M] [hSM : 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_4} {S : Type u_5} [ M] [hSM : 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_4} {S : Type u_5} [ M] [hSM : M] {K : S} {x : M} (hx : x K) (n : ) :
x ^ n K
theorem zsmul_mem {M : Type u_4} {S : Type u_5} [ M] [hSM : M] {K : S} {x : M} (hx : x K) (n : ) :
n x K
theorem sub_mem_comm_iff {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [ G] [hSG : G] {a b : G} :
a - b H b - a H
theorem div_mem_comm_iff {G : Type u_1} [group G] {S : Type u_5} {H : S} [ G] [hSG : G] {a b : G} :
a / b H b / a H
@[simp]
theorem exists_neg_mem_iff_exists_mem {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : G] {x y : G} (h : x H) :
x * y H y H
@[protected, instance]
def add_subgroup_class.has_neg {M : Type u_4} {S : Type u_5} [ M] [hSM : M] {H : S} :

An additive subgroup of a `add_group` inherits an inverse.

Equations
@[protected, instance]
def subgroup_class.has_inv {M : Type u_4} {S : Type u_5} [ M] [hSM : M] {H : S} :

A subgroup of a group inherits an inverse.

Equations
@[protected, instance]
def subgroup_class.has_div {M : Type u_4} {S : Type u_5} [ M] [hSM : M] {H : S} :

A subgroup of a group inherits a division

Equations
@[protected, instance]
def add_subgroup_class.has_sub {M : Type u_4} {S : Type u_5} [ M] [hSM : 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} [ M] [ 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_4} {S : Type u_5} [ M] [hSM : 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_4} {S : Type u_5} [ M] [hSM : M] {H : S} (x : H) :
@[simp, norm_cast]
theorem subgroup_class.coe_inv {M : Type u_4} {S : Type u_5} [ M] [hSM : M] {H : S} (x : H) :
@[simp, norm_cast]
theorem subgroup_class.coe_div {M : Type u_4} {S : Type u_5} [ M] [hSM : M] {H : S} (x y : H) :
(x / y) = x / y
@[simp, norm_cast]
theorem add_subgroup_class.coe_sub {M : Type u_4} {S : Type u_5} [ M] [hSM : 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_5} (H : S) [ G] [hSG : 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_5} (H : S) [ G] [hSG : 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_5} (H : S) {G : Type u_1} [comm_group G] [ G] [ 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_5} (H : S) {G : Type u_1} [ G] [ G] :

An additive subgroup of an `add_comm_group` is an `add_comm_group`.

Equations
@[protected, instance]
def add_subgroup_class.to_ordered_add_comm_group {S : Type u_5} (H : S) {G : Type u_1} [ G] [ G] :

An additive subgroup of an `add_ordered_comm_group` is an `add_ordered_comm_group`.

Equations
@[protected, instance]
def subgroup_class.to_ordered_comm_group {S : Type u_5} (H : S) {G : Type u_1} [ G] [ G] :

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

Equations
@[protected, instance]
def add_subgroup_class.to_linear_ordered_add_comm_group {S : Type u_5} (H : S) {G : Type u_1} [ G] [ G] :

An additive subgroup of a `linear_ordered_add_comm_group` is a `linear_ordered_add_comm_group`.

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

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

Equations
@[protected]
def add_subgroup_class.subtype {G : Type u_1} [add_group G] {S : Type u_5} (H : S) [ G] [hSG : G] :

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

Equations
@[protected]
def subgroup_class.subtype {G : Type u_1} [group G] {S : Type u_5} (H : S) [ G] [hSG : 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_5} (H : S) [ G] [hSG : G] :
@[simp]
theorem subgroup_class.coe_subtype {G : Type u_1} [group G] {S : Type u_5} (H : S) [ G] [hSG : G] :
@[simp, norm_cast]
theorem add_subgroup_class.coe_smul {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : 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_5} {H : S} [ G] [hSG : G] (x : H) (n : ) :
(x ^ n) = x ^ n
def add_subgroup_class.inclusion {G : Type u_1} [add_group G] {S : Type u_5} [ G] [hSG : 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_5} [ G] [hSG : 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_5} {H : S} [ G] [hSG : G] (x : H) :
@[simp]
theorem subgroup_class.inclusion_self {G : Type u_1} [group G] {S : Type u_5} {H : S} [ G] [hSG : G] (x : H) :
@[simp]
theorem add_subgroup_class.inclusion_mk {G : Type u_1} [add_group G] {S : Type u_5} {H K : S} [ G] [hSG : G] {h : H K} (x : G) (hx : x H) :
x, hx⟩ = x, _⟩
@[simp]
theorem subgroup_class.inclusion_mk {G : Type u_1} [group G] {S : Type u_5} {H K : S} [ G] [hSG : G] {h : H K} (x : G) (hx : x H) :
x, hx⟩ = x, _⟩
theorem subgroup_class.inclusion_right {G : Type u_1} [group G] {S : Type u_5} {H K : S} [ G] [hSG : G] (h : H K) (x : K) (hx : x H) :
x, hx⟩ = x
theorem add_subgroup_class.inclusion_right {G : Type u_1} [add_group G] {S : Type u_5} {H K : S} [ G] [hSG : G] (h : H K) (x : K) (hx : x H) :
x, hx⟩ = x
@[simp]
theorem subgroup_class.inclusion_inclusion {G : Type u_1} [group G] {S : Type u_5} {H K : S} [ G] [hSG : G] {L : S} (hHK : H K) (hKL : K L) (x : H) :
( x) =
@[simp]
theorem add_subgroup_class.coe_inclusion {G : Type u_1} [add_group G] {S : Type u_5} [ G] [hSG : G] {H K : S} {h : H K} (a : H) :
@[simp]
theorem subgroup_class.coe_inclusion {G : Type u_1} [group G] {S : Type u_5} [ G] [hSG : G] {H K : S} {h : H K} (a : H) :
a) = a
@[simp]
theorem add_subgroup_class.subtype_comp_inclusion {G : Type u_1} [add_group G] {S : Type u_5} [ G] [hSG : G] {H K : S} (hH : H K) :
@[simp]
theorem subgroup_class.subtype_comp_inclusion {G : Type u_1} [group G] {S : Type u_5} [ G] [hSG : G] {H K : S} (hH : H K) :
def subgroup.to_submonoid {G : Type u_4} [group G] (self : subgroup G) :

Reinterpret a `subgroup` as a `submonoid`.

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

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

Instances for `subgroup`
Type u_4

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

Instances for `add_subgroup`

Reinterpret an `add_subgroup` as an `add_submonoid`.

@[protected, instance]
def subgroup.set_like {G : Type u_1} [group G] :
Equations
@[protected, instance]
G
Equations
@[protected, instance]
@[protected, instance]
def subgroup.subgroup_class {G : Type u_1} [group G] :
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
@[simp]
theorem add_subgroup.mem_mk {G : Type u_1} [add_group G] {s : set G} {x : G} (h_one : {a b : G}, a s b s a + 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 s b s a * b s) (h_mul : 1 s) (h_inv : {x : G}, x s x⁻¹ 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 s b s a * b s) (h_mul : 1 s) (h_inv : {x : G}, x s x⁻¹ 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 s b s a + 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 s b s a + b s) (h_mul : 0 s) (h_inv : {x : G}, x s -x s) (h_one' : {a b : G}, a t b t a + 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 s b s a * b s) (h_mul : 1 s) (h_inv : {x : G}, x s x⁻¹ s) (h_one' : {a b : G}, a t b t a * b t) (h_mul' : 1 t) (h_inv' : {x : G}, x t x⁻¹ 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
Equations
set G
Equations
@[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
@[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_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]
@[reducible]
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]
@[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_subgroup`s 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]
0 H

An `add_subgroup` contains the group's 0.

@[protected]
x H y H x + 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 H y H x * 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 H x⁻¹ H

A subgroup is closed under inverse.

@[protected]
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]
-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 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]
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]
x + y H y H
@[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 s x * 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 s x + -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]

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]

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

Equations
@[protected, instance]

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]

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

Equations
@[protected, instance]

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]

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]
(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 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
@[simp]
theorem subgroup.mk_eq_one_iff {G : Type u_1} [group G] (H : subgroup G) {g : G} {h : g H} :
g, h⟩ = 1 g = 1
@[simp]
theorem add_subgroup.mk_eq_zero_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {g : G} {h : g H} :
g, h⟩ = 0 g = 0
@[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.

Equations
@[protected, instance]

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

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

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

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

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 subgroup.subtype_injective {G : Type u_1} [group G] (H : subgroup G) :
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) :
( 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
theorem add_subgroup.inclusion_injective {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :
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]

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]
theorem add_subgroup.top_equiv_apply {G : Type u_1} [add_group G] (x : ) :
@[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

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]

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]
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]
@[simp]
= {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
@[simp]
theorem subgroup.top_to_submonoid {G : Type u_1} [group G] :
@[simp]
@[simp]
@[simp]
theorem subgroup.bot_to_submonoid {G : Type u_1} [group G] :
theorem subgroup.eq_bot_iff_forall {G : Type u_1} [group G] (H : subgroup G) :
H = (x : G), x H x = 1
H = (x : G), x H x = 0
theorem subgroup.eq_bot_of_subsingleton {G : Type u_1} [group G] (H : subgroup G)  :
H =
theorem subgroup.coe_eq_univ {G : Type u_1} [group G] {H : subgroup G} :
H =
H =
( (g : G), H = {g}) H =
theorem subgroup.coe_eq_singleton {G : Type u_1} [group G] {H : subgroup G} :
( (g : G), H = {g}) 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 =

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.

H = (x : G) (H : x H), x 0

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

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

Equations
@[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]
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]
(has_Inf.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 (p : , p S x p
@[simp]
theorem subgroup.mem_Inf {G : Type u_1} [group G] {S : set (subgroup G)} {x : G} :
x (p : subgroup G), p S x 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.

Equations
theorem subgroup.mem_sup_left {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x S x S T
theorem add_subgroup.mem_sup_left {G : Type u_1} [add_group G] {S T : add_subgroup G} {x : G} :
x S x S T
theorem subgroup.mem_sup_right {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x T x S T
theorem add_subgroup.mem_sup_right {G : Type u_1} [add_group G] {S T : add_subgroup G} {x : G} :
x T x 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 : ι } (i : ι) {x : G} :
x S i x supr S
theorem add_subgroup.mem_supr_of_mem {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι } (i : ι) {x : G} :
x S i x 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 s x
theorem add_subgroup.mem_Sup_of_mem {G : Type u_1} [add_group G] {S : set (add_subgroup G)} {s : add_subgroup G} (hs : s S) {x : G} :
x s x
@[simp]
theorem subgroup.subsingleton_iff {G : Type u_1} [group G] :
@[simp]
@[simp]
theorem subgroup.nontrivial_iff {G : Type u_1} [group G] :
@[simp]
@[protected, instance]
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]
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} :
(K : subgroup G), k K x K
theorem add_subgroup.mem_closure {G : Type u_1} [add_group G] {k : set G} {x : G} :
(K : , k K x 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.

theorem add_subgroup.not_mem_of_not_mem_closure {G : Type u_1} [add_group G] {k : set G} {P : G} (hP : P ) :
P k
theorem subgroup.not_mem_of_not_mem_closure {G : Type u_1} [group G] {k : set G} {P : G} (hP : P ) :
P k
@[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 k p x) (H1 : p 1) (Hmul : (x y : G), p x p y p (x * y)) (Hinv : (x : G), p x p x⁻¹) :
p x

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

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

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

theorem subgroup.closure_induction' {G : Type u_1} [group G] {k : set G} {p : Π (x : G), Prop} (Hs : (x : G) (h : x k), p x _) (H1 : p 1 _) (Hmul : (x : G) (hx : (y : G) (hy : , p x hx p y hy p (x * y) _) (Hinv : (x : G) (hx : , p x hx p x⁻¹ _) {x : G} (hx : x ) :
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), Prop} (Hs : (x : G) (h : x k), p x _) (H1 : p 0 _) (Hmul : (x : G) (hx : (y : G) (hy : , p x hx p y hy p (x + y) _) (Hinv : (x : G) (hx : , p x hx p (-x) _) {x : G} (hx : x ) :
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 ) (hy : y ) (Hk : (x : G), x k (y : G), y k p x y) (H1_left : (x : G), p 0 x) (H1_right : (x : G), p x 0) (Hmul_left : (x₁ x₂ y : G), p x₁ y p x₂ y p (x₁ + x₂) y) (Hmul_right : (x y₁ y₂ : G), p x y₁ p x y₂ p x (y₁ + y₂)) (Hinv_left : (x y : G), p x y p (-x) y) (Hinv_right : (x y : G), p x y p x (-y)) :
p x y

An induction principle for additive closure membership, for predicates with two arguments.

theorem subgroup.closure_induction₂ {G : Type u_1} [group G] {k : set G} {p : G G Prop} {x y : G} (hx : x ) (hy : y ) (Hk : (x : G), x k (y : G), y k p x y) (H1_left : (x : G), p 1 x) (H1_right : (x : G), p x 1) (Hmul_left : (x₁ x₂ y : G), p x₁ y p x₂ y p (x₁ * x₂) y) (Hmul_right : (x y₁ y₂ : G), p x y₁ p x y₂ p x (y₁ * y₂)) (Hinv_left : (x y : G), p x y p x⁻¹ y) (Hinv_right : (x y : G), p x y p x y⁻¹) :
p x y

An induction principle for closure membership for predicates with two arguments.

@[simp]
theorem subgroup.closure_closure_coe_preimage {G : Type u_1} [group G] {k : set G} :
@[simp]
theorem add_subgroup.closure_closure_coe_preimage {G : Type u_1} [add_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 k x * y = y * x) :

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

Equations
def add_subgroup.closure_add_comm_group_of_comm {G : Type u_1} [add_group G] {k : set G} (hcomm : (x : G), x k (y : G), y k x + y = y + x) :

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

Equations
@[protected]

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

Equations
@[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.supr_eq_closure {G : Type u_1} [group G] {ι : Sort u_2} (p : ι ) :
( (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 : ι ) :
( (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} :
(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 (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] :
theorem subgroup.le_closure_to_submonoid {G : Type u_1} [group G] (S : set G) :
theorem subgroup.closure_eq_top_of_mclosure_eq_top {G : Type u_1} [group G] {S : set G} (h : = ) :
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 (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 (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
Instances for `subgroup.comap`
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`.

Equations
Instances for `add_subgroup.comap`
@[simp]
theorem subgroup.coe_comap {G : Type u_1} [group G] {N : Type u_4} [group N] (K : subgroup N) (f : G →* N) :
@[simp]
theorem add_subgroup.coe_comap {G : Type u_1} [add_group G] {N : Type u_4} [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_4} [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_4} [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_4} [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_4} [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_4} [add_group N] {P : Type u_5} [