mathlib3 documentation

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:

Definitions in the file:

Implementation notes #

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

Tags #

subgroup, subgroups

@[class]
structure inv_mem_class (S : Type u_4) (G : Type u_5) [has_inv G] [set_like S 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] [set_like S 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) [div_inv_monoid G] [set_like S G] :
Prop

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) [sub_neg_monoid G] [set_like S G] :
Prop

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} [has_involutive_neg G] [set_like S G] [neg_mem_class S G] {H : S} {x : G} :
-x H x H
@[simp]
theorem inv_mem_iff {S : Type u_1} {G : Type u_2} [has_involutive_inv G] [set_like S G] [inv_mem_class S G] {H : S} {x : G} :
x⁻¹ H x H
theorem div_mem {M : Type u_4} {S : Type u_5} [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M] {H : S} {x y : M} (hx : x H) (hy : y H) :
x / y H

A subgroup is closed under division.

theorem sub_mem {M : Type u_4} {S : Type u_5} [sub_neg_monoid M] [set_like S M] [hSM : add_subgroup_class S M] {H : S} {x y : M} (hx : x H) (hy : y H) :
x - y H

An additive subgroup is closed under subtraction.

theorem zpow_mem {M : Type u_4} {S : Type u_5} [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M] {K : S} {x : M} (hx : x K) (n : ) :
x ^ n K
theorem zsmul_mem {M : Type u_4} {S : Type u_5} [sub_neg_monoid M] [set_like S M] [hSM : add_subgroup_class S M] {K : S} {x : M} (hx : x K) (n : ) :
n x K
theorem sub_mem_comm_iff {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [set_like S G] [hSG : add_subgroup_class S G] {a b : G} :
a - b H b - a H
theorem div_mem_comm_iff {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S 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} [set_like S G] [hSG : add_subgroup_class S G] {P : G Prop} :
( (x : G), x H P (-x)) (x : G) (H : x H), P x
@[simp]
theorem exists_inv_mem_iff_exists_mem {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S G] {P : G Prop} :
( (x : G), x H P x⁻¹) (x : G) (H : x H), P x
theorem add_mem_cancel_right {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [set_like S G] [hSG : add_subgroup_class S G] {x y : G} (h : x H) :
y + x H y H
theorem mul_mem_cancel_right {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S G] {x y : G} (h : x H) :
y * x H y H
theorem add_mem_cancel_left {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [set_like S G] [hSG : add_subgroup_class S G] {x y : G} (h : x H) :
x + y H y H
theorem mul_mem_cancel_left {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S G] {x y : G} (h : x H) :
x * y H y H
@[protected, instance]
def add_subgroup_class.has_neg {M : Type u_4} {S : Type u_5} [sub_neg_monoid M] [set_like S M] [hSM : add_subgroup_class S M] {H : S} :

An additive subgroup of a add_group inherits an inverse.

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

A subgroup of a group inherits an inverse.

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

A subgroup of a group inherits a division

Equations
@[protected, instance]
def add_subgroup_class.has_sub {M : Type u_4} {S : Type u_5} [sub_neg_monoid M] [set_like S M] [hSM : add_subgroup_class S M] {H : S} :

An additive subgroup of an add_group inherits a subtraction.

Equations
@[protected, instance]
def add_subgroup_class.has_zsmul {M : Type u_1} {S : Type u_2} [sub_neg_monoid M] [set_like S M] [add_subgroup_class S M] {H : S} :

An additive subgroup of an add_group inherits an integer scaling.

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

A subgroup of a group inherits an integer power.

Equations
@[simp, norm_cast]
theorem add_subgroup_class.coe_neg {M : Type u_4} {S : Type u_5} [sub_neg_monoid M] [set_like S M] [hSM : add_subgroup_class S M] {H : S} (x : H) :
@[simp, norm_cast]
theorem subgroup_class.coe_inv {M : Type u_4} {S : Type u_5} [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M] {H : S} (x : H) :
@[simp, norm_cast]
theorem subgroup_class.coe_div {M : Type u_4} {S : Type u_5} [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M] {H : S} (x y : H) :
(x / y) = x / y
@[simp, norm_cast]
theorem add_subgroup_class.coe_sub {M : Type u_4} {S : Type u_5} [sub_neg_monoid M] [set_like S M] [hSM : add_subgroup_class S M] {H : S} (x y : H) :
(x - y) = x - y
@[protected, instance]
def subgroup_class.to_group {G : Type u_1} [group G] {S : Type u_5} (H : S) [set_like S G] [hSG : subgroup_class S G] :

A subgroup of a group inherits a group structure.

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

An additive subgroup of an add_group inherits an add_group structure.

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

A subgroup of a comm_group is a comm_group.

Equations
@[protected, instance]

An additive subgroup of an add_comm_group is an add_comm_group.

Equations
@[protected, instance]

An additive subgroup of an add_ordered_comm_group is an add_ordered_comm_group.

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

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

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

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

Equations
@[simp]
theorem add_subgroup_class.coe_subtype {G : Type u_1} [add_group G] {S : Type u_5} (H : S) [set_like S G] [hSG : add_subgroup_class S G] :
@[simp]
theorem subgroup_class.coe_subtype {G : Type u_1} [group G] {S : Type u_5} (H : S) [set_like S G] [hSG : subgroup_class S G] :
@[simp, norm_cast]
theorem add_subgroup_class.coe_smul {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [set_like S G] [hSG : add_subgroup_class S G] (x : H) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem subgroup_class.coe_pow {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S G] (x : H) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem add_subgroup_class.coe_zsmul {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [set_like S G] [hSG : add_subgroup_class S G] (x : H) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem subgroup_class.coe_zpow {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S G] (x : H) (n : ) :
(x ^ n) = x ^ n
def add_subgroup_class.inclusion {G : Type u_1} [add_group G] {S : Type u_5} [set_like S G] [hSG : add_subgroup_class S G] {H K : S} (h : H K) :

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

Equations
def subgroup_class.inclusion {G : Type u_1} [group G] {S : Type u_5} [set_like S G] [hSG : subgroup_class S G] {H K : S} (h : H K) :

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

Equations
@[simp]
theorem add_subgroup_class.inclusion_self {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [set_like S G] [hSG : add_subgroup_class S G] (x : H) :
@[simp]
theorem subgroup_class.inclusion_self {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S G] (x : H) :
@[simp]
theorem add_subgroup_class.inclusion_mk {G : Type u_1} [add_group G] {S : Type u_5} {H K : S} [set_like S G] [hSG : add_subgroup_class S G] {h : H K} (x : G) (hx : x H) :
@[simp]
theorem subgroup_class.inclusion_mk {G : Type u_1} [group G] {S : Type u_5} {H K : S} [set_like S G] [hSG : subgroup_class S G] {h : H K} (x : G) (hx : x H) :
theorem subgroup_class.inclusion_right {G : Type u_1} [group G] {S : Type u_5} {H K : S} [set_like S G] [hSG : subgroup_class S G] (h : H K) (x : K) (hx : x H) :
theorem add_subgroup_class.inclusion_right {G : Type u_1} [add_group G] {S : Type u_5} {H K : S} [set_like S G] [hSG : add_subgroup_class S G] (h : H K) (x : K) (hx : x H) :
@[simp]
theorem subgroup_class.inclusion_inclusion {G : Type u_1} [group G] {S : Type u_5} {H K : S} [set_like S G] [hSG : subgroup_class S G] {L : S} (hHK : H K) (hKL : K L) (x : H) :
@[simp]
theorem add_subgroup_class.coe_inclusion {G : Type u_1} [add_group G] {S : Type u_5} [set_like S G] [hSG : add_subgroup_class S G] {H K : S} {h : H K} (a : H) :
@[simp]
theorem subgroup_class.coe_inclusion {G : Type u_1} [group G] {S : Type u_5} [set_like S G] [hSG : subgroup_class S G] {H K : S} {h : H K} (a : H) :
@[simp]
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
structure add_subgroup (G : Type u_4) [add_group G] :
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
@[protected, instance]
def subgroup.set_like {G : Type u_1} [group G] :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[simp]
theorem subgroup.mem_carrier {G : Type u_1} [group G] {s : subgroup G} {x : G} :
x s.carrier x s
@[simp]
theorem add_subgroup.mem_carrier {G : Type u_1} [add_group G] {s : add_subgroup G} {x : G} :
x s.carrier x s
@[simp]
theorem add_subgroup.mem_mk {G : Type u_1} [add_group G] {s : set G} {x : G} (h_one : {a b : G}, a 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
@[simp]
theorem subgroup.coe_to_submonoid {G : Type u_1} [group G] (K : subgroup G) :
@[simp]
theorem subgroup.mem_to_submonoid {G : Type u_1} [group G] (K : subgroup G) (x : G) :
@[simp]
theorem add_subgroup.mem_to_add_submonoid {G : Type u_1} [add_group G] (K : add_subgroup G) (x : G) :
@[simp]
theorem subgroup.to_submonoid_eq {G : Type u_1} [group G] {p q : subgroup G} :
@[simp]
theorem subgroup.to_submonoid_le {G : Type u_1} [group G] {p q : subgroup G} :

Conversion to/from additive/multiplicative #

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

Equations
@[reducible]

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

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

Equations
@[reducible]

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

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

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

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

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

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

Two subgroups are equal if they have the same elements.

@[ext]
theorem add_subgroup.ext {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : (x : G), x H x K) :
H = K

Two add_subgroups are equal if they have the same elements.

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

A subgroup contains the group's 1.

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

An add_subgroup contains the group's 0.

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

An add_subgroup is closed under inverse.

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

A subgroup is closed under division.

@[protected]
theorem add_subgroup.sub_mem {G : Type u_1} [add_group G] (H : add_subgroup G) {x y : G} (hx : x H) (hy : y H) :
x - y H

An add_subgroup is closed under subtraction.

@[protected]
theorem add_subgroup.neg_mem_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {x : G} :
-x H x H
@[protected]
theorem subgroup.inv_mem_iff {G : Type u_1} [group G] (H : subgroup G) {x : G} :
x⁻¹ H x H
@[protected]
theorem add_subgroup.sub_mem_comm_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {a b : G} :
a - b H b - a H
@[protected]
theorem subgroup.div_mem_comm_iff {G : Type u_1} [group G] (H : subgroup G) {a b : G} :
a / b H b / a H
@[protected]
theorem subgroup.exists_inv_mem_iff_exists_mem {G : Type u_1} [group G] (K : subgroup G) {P : G Prop} :
( (x : G), x K P x⁻¹) (x : G) (H : x K), P x
@[protected]
theorem add_subgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {P : G Prop} :
( (x : G), x K P (-x)) (x : G) (H : x K), P x
@[protected]
theorem add_subgroup.add_mem_cancel_right {G : Type u_1} [add_group G] (H : add_subgroup G) {x y : G} (h : x H) :
y + x H y H
@[protected]
theorem subgroup.mul_mem_cancel_right {G : Type u_1} [group G] (H : subgroup G) {x y : G} (h : x H) :
y * x H y H
@[protected]
theorem subgroup.mul_mem_cancel_left {G : Type u_1} [group G] (H : subgroup G) {x y : G} (h : x H) :
x * y H y H
@[protected]
theorem add_subgroup.add_mem_cancel_left {G : Type u_1} [add_group G] (H : add_subgroup G) {x y : G} (h : x H) :
x + y H y H
@[protected]
theorem subgroup.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]
def add_subgroup.has_add {G : Type u_1} [add_group G] (H : add_subgroup G) :

An add_subgroup of an add_group inherits an addition.

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

A subgroup of a group inherits a 1.

Equations
@[protected, instance]

An add_subgroup of an add_group inherits a zero.

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

A add_subgroup of a add_group inherits an inverse.

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

A subgroup of a group inherits an inverse.

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

A subgroup of a group inherits a division

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

An add_subgroup of an add_group inherits a subtraction.

Equations
@[protected, instance]

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]
theorem add_subgroup.coe_add {G : Type u_1} [add_group G] (H : add_subgroup G) (x y : H) :
(x + y) = x + y
@[simp, norm_cast]
theorem subgroup.coe_mul {G : Type u_1} [group G] (H : subgroup G) (x y : H) :
(x * y) = x * y
@[simp, norm_cast]
theorem add_subgroup.coe_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
0 = 0
@[simp, norm_cast]
theorem subgroup.coe_one {G : Type u_1} [group G] (H : subgroup G) :
1 = 1
@[simp, norm_cast]
theorem add_subgroup.coe_neg {G : Type u_1} [add_group G] (H : add_subgroup G) (x : H) :
@[simp, norm_cast]
theorem subgroup.coe_inv {G : Type u_1} [group G] (H : subgroup G) (x : H) :
@[simp, norm_cast]
theorem subgroup.coe_div {G : Type u_1} [group G] (H : subgroup G) (x y : H) :
(x / y) = x / y
@[simp, norm_cast]
theorem add_subgroup.coe_sub {G : Type u_1} [add_group G] (H : add_subgroup G) (x y : H) :
(x - y) = x - y
@[simp, norm_cast]
theorem add_subgroup.coe_mk {G : Type u_1} [add_group G] (H : add_subgroup G) (x : G) (hx : x H) :
x, hx⟩ = x
@[simp, norm_cast]
theorem subgroup.coe_mk {G : Type u_1} [group G] (H : subgroup G) (x : G) (hx : x H) :
x, hx⟩ = x
@[simp, norm_cast]
theorem subgroup.coe_pow {G : Type u_1} [group G] (H : subgroup G) (x : H) (n : ) :
(x ^ n) = x ^ n
@[simp, norm_cast]
theorem add_subgroup.coe_nsmul {G : Type u_1} [add_group G] (H : add_subgroup G) (x : H) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem add_subgroup.coe_zsmul {G : Type u_1} [add_group G] (H : add_subgroup G) (x : H) (n : ) :
(n x) = n x
@[simp, norm_cast]
theorem subgroup.coe_zpow {G : Type u_1} [group G] (H : subgroup G) (x : H) (n : ) :
(x ^ n) = x ^ n
@[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]

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]
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]
def add_subgroup.subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :

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

Equations
@[simp]
theorem subgroup.coe_subtype {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem add_subgroup.coe_subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :
def add_subgroup.inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :

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

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

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

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

The top additive subgroup is isomorphic to the additive group.

This is the additive group version of add_submonoid.top_equiv.

Equations
@[simp]
@[protected, instance]

The trivial add_subgroup {0} of an add_group G.

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]
theorem add_subgroup.coe_top {G : Type u_1} [add_group G] :
@[simp]
theorem add_subgroup.coe_bot {G : Type u_1} [add_group G] :
= {0}
@[simp]
theorem subgroup.coe_bot {G : Type u_1} [group G] :
= {1}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem subgroup.eq_bot_iff_forall {G : Type u_1} [group G] (H : subgroup G) :
H = (x : G), x H x = 1
theorem add_subgroup.eq_bot_iff_forall {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = (x : G), x H x = 0
theorem subgroup.coe_eq_univ {G : Type u_1} [group G] {H : subgroup G} :
theorem add_subgroup.coe_eq_singleton {G : Type u_1} [add_group G] {H : add_subgroup G} :
( (g : G), H = {g}) H =
theorem subgroup.coe_eq_singleton {G : Type u_1} [group G] {H : subgroup G} :
( (g : G), H = {g}) H =
theorem add_subgroup.nontrivial_iff_exists_ne_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
nontrivial H (x : G) (H : x H), x 0
theorem subgroup.nontrivial_iff_exists_ne_one {G : Type u_1} [group G] (H : subgroup G) :
nontrivial H (x : G) (H : x H), x 1
theorem subgroup.bot_or_nontrivial {G : Type u_1} [group G] (H : subgroup G) :

A subgroup is either the trivial subgroup or nontrivial.

A subgroup is either the trivial subgroup or nontrivial.

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

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

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

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

@[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_subgroupss is their intersection.

Equations
@[simp]
theorem subgroup.coe_inf {G : Type u_1} [group G] (p p' : subgroup G) :
(p p') = p p'
@[simp]
theorem add_subgroup.coe_inf {G : Type u_1} [add_group G] (p p' : add_subgroup G) :
(p p') = p p'
@[simp]
theorem add_subgroup.mem_inf {G : Type u_1} [add_group G] {p p' : add_subgroup G} {x : G} :
x p p' x p x p'
@[simp]
theorem subgroup.mem_inf {G : Type u_1} [group G] {p p' : subgroup G} {x : G} :
x p p' x p x p'
@[protected, instance]
Equations
@[protected, instance]
def subgroup.has_Inf {G : Type u_1} [group G] :
Equations
@[simp, norm_cast]
theorem subgroup.coe_Inf {G : Type u_1} [group G] (H : set (subgroup G)) :
(has_Inf.Inf H) = (s : subgroup G) (H : s H), s
@[simp, norm_cast]
theorem add_subgroup.coe_Inf {G : Type u_1} [add_group G] (H : set (add_subgroup G)) :
(has_Inf.Inf H) = (s : add_subgroup G) (H : s H), s
@[simp]
theorem add_subgroup.mem_Inf {G : Type u_1} [add_group G] {S : set (add_subgroup G)} {x : G} :
x has_Inf.Inf S (p : add_subgroup G), p S x p
@[simp]
theorem subgroup.mem_Inf {G : Type u_1} [group G] {S : set (subgroup G)} {x : G} :
x has_Inf.Inf S (p : subgroup G), p S x p
theorem subgroup.mem_infi {G : Type u_1} [group G] {ι : Sort u_2} {S : ι subgroup G} {x : G} :
(x (i : ι), S i) (i : ι), x S i
theorem add_subgroup.mem_infi {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι add_subgroup G} {x : G} :
(x (i : ι), S i) (i : ι), x S i
@[simp, norm_cast]
theorem subgroup.coe_infi {G : Type u_1} [group G] {ι : Sort u_2} {S : ι subgroup G} :
( (i : ι), S i) = (i : ι), (S i)
@[simp, norm_cast]
theorem add_subgroup.coe_infi {G : Type u_1} [add_group G] {ι : Sort u_2} {S : ι add_subgroup G} :
( (i : ι), S i) = (i : ι), (S i)
@[protected, instance]

Subgroups of a group form a complete lattice.

Equations
@[protected, instance]

The add_subgroups of an add_group form a complete lattice.

Equations
theorem subgroup.mem_sup_left {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x 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 : ι subgroup G} (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 : ι add_subgroup G} (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} :
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} :
@[simp]
@[protected, instance]
Equations
@[protected, instance]
def subgroup.unique {G : Type u_1} [group G] [subsingleton G] :
Equations
@[protected, instance]
@[protected, instance]
theorem add_subgroup.eq_top_iff' {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = (x : G), x H
theorem subgroup.eq_top_iff' {G : Type u_1} [group G] (H : subgroup G) :
H = (x : G), x H
def add_subgroup.closure {G : Type u_1} [add_group G] (k : set G) :

The add_subgroup generated by a set

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

The subgroup generated by a set.

Equations
Instances for subgroup.closure
theorem subgroup.mem_closure {G : Type u_1} [group G] {k : set G} {x : G} :
theorem add_subgroup.mem_closure {G : Type u_1} [add_group G] {k : set G} {x : G} :
@[simp]
theorem subgroup.subset_closure {G : Type u_1} [group G] {k : set G} :

The subgroup generated by a set includes the set.

@[simp]
theorem add_subgroup.subset_closure {G : Type u_1} [add_group G] {k : set G} :

The add_subgroup generated by a set includes the set.

theorem add_subgroup.not_mem_of_not_mem_closure {G : Type u_1} [add_group G] {k : set G} {P : G} (hP : P add_subgroup.closure k) :
P k
theorem subgroup.not_mem_of_not_mem_closure {G : Type u_1} [group G] {k : set G} {P : G} (hP : P subgroup.closure k) :
P k
@[simp]
theorem subgroup.closure_le {G : Type u_1} [group G] (K : subgroup G) {k : set G} :

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

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

An additive subgroup K includes closure k if and only if it includes k

theorem subgroup.closure_eq_of_le {G : Type u_1} [group G] (K : subgroup G) {k : set G} (h₁ : k K) (h₂ : K subgroup.closure k) :
theorem add_subgroup.closure_eq_of_le {G : Type u_1} [add_group G] (K : add_subgroup G) {k : set G} (h₁ : k K) (h₂ : K add_subgroup.closure k) :
theorem subgroup.closure_induction {G : Type u_1} [group G] {k : set G} {p : G Prop} {x : G} (h : x subgroup.closure k) (Hk : (x : G), x k p x) (H1 : p 1) (Hmul : (x y : G), p x p y p (x * y)) (Hinv : (x : G), p x p x⁻¹) :
p x

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

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

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

theorem subgroup.closure_induction' {G : Type u_1} [group G] {k : set G} {p : Π (x : G), x subgroup.closure k Prop} (Hs : (x : G) (h : x k), p x _) (H1 : p 1 _) (Hmul : (x : G) (hx : x subgroup.closure k) (y : G) (hy : y subgroup.closure k), p x hx p y hy p (x * y) _) (Hinv : (x : G) (hx : x subgroup.closure k), p x hx p x⁻¹ _) {x : G} (hx : x subgroup.closure k) :
p x hx

A dependent version of subgroup.closure_induction.

theorem add_subgroup.closure_induction' {G : Type u_1} [add_group G] {k : set G} {p : Π (x : G), x add_subgroup.closure k Prop} (Hs : (x : G) (h : x k), p x _) (H1 : p 0 _) (Hmul : (x : G) (hx : x add_subgroup.closure k) (y : G) (hy : y add_subgroup.closure k), p x hx p y hy p (x + y) _) (Hinv : (x : G) (hx : x add_subgroup.closure k), p x hx p (-x) _) {x : G} (hx : x add_subgroup.closure k) :
p x hx

A dependent version of add_subgroup.closure_induction.

theorem add_subgroup.closure_induction₂ {G : Type u_1} [add_group G] {k : set G} {p : G G Prop} {x y : G} (hx : x add_subgroup.closure k) (hy : y add_subgroup.closure k) (Hk : (x : G), x k (y : G), y k p x y) (H1_left : (x : G), p 0 x) (H1_right : (x : G), p x 0) (Hmul_left : (x₁ x₂ y : G), p x₁ y p x₂ y p (x₁ + x₂) y) (Hmul_right : (x y₁ y₂ : G), p x y₁ p x y₂ p x (y₁ + y₂)) (Hinv_left : (x y : G), p x y p (-x) y) (Hinv_right : (x y : G), p x y p x (-y)) :
p x y

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

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

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

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

closure forms a Galois insertion with the coercion to set.

Equations
@[protected]

closure forms a Galois insertion with the coercion to set.

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

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

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

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

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

Closure of a subgroup K equals K.

@[simp]

Additive closure of an additive subgroup K equals K

@[simp]
theorem subgroup.closure_Union {G : Type u_1} [group G] {ι : Sort u_2} (s : ι set G) :
subgroup.closure ( (i : ι), s i) = (i : ι), subgroup.closure (s i)
theorem add_subgroup.closure_Union {G : Type u_1} [add_group G] {ι : Sort u_2} (s : ι set G) :
add_subgroup.closure ( (i : ι), s i) = (i : ι), add_subgroup.closure (s i)
theorem subgroup.closure_eq_bot_iff (G : Type u_1) [group G] (S : set G) :
theorem subgroup.supr_eq_closure {G : Type u_1} [group G] {ι : Sort u_2} (p : ι subgroup G) :
( (i : ι), p i) = subgroup.closure ( (i : ι), (p i))
theorem add_subgroup.supr_eq_closure {G : Type u_1} [add_group G] {ι : Sort u_2} (p : ι add_subgroup G) :
( (i : ι), p i) = add_subgroup.closure ( (i : ι), (p i))
theorem add_subgroup.mem_closure_singleton {G : Type u_1} [add_group G] {x y : G} :

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

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

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

theorem add_subgroup.mem_supr_of_directed {G : Type u_1} [add_group G] {ι : Sort u_2} [hι : nonempty ι] {K : ι add_subgroup G} (hK : directed has_le.le 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 : ι subgroup G} (hK : directed has_le.le 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 : ι subgroup G} (hS : directed has_le.le 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 : ι add_subgroup G} (hS : directed has_le.le 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 : directed_on has_le.le K) {x : G} :
x has_Sup.Sup K (s : add_subgroup G) (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 : directed_on has_le.le K) {x : G} :
x has_Sup.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
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} :
@[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} :
theorem subgroup.comap_mono {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {K K' : subgroup N} :
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} :
theorem add_subgroup.comap_comap {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {P : Type u_5} [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_4} [group N] {P : Type u_5} [group P] (K : subgroup P) (g : N →* P) (f : G →* N) :
@[simp]
theorem subgroup.comap_id {N : Type u_4} [group N] (K : subgroup N) :
def add_subgroup.map {G : Type u_1} [add_group G] {N : Type u_4} [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.

Equations
Instances for add_subgroup.map
def subgroup.map {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H : subgroup G) :

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

Equations
Instances for subgroup.map
@[simp]
theorem add_subgroup.coe_map {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) (K : add_subgroup G) :
@[simp]
theorem subgroup.coe_map {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (K : subgroup G) :
@[simp]
theorem add_subgroup.mem_map {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {K : add_subgroup G} {y : N} :
y add_subgroup.map f K (x : G) (H : x K), f x = y
@[simp]
theorem subgroup.mem_map {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {K : subgroup G} {y : N} :
y subgroup.map f 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_4} [add_group N] (f : G →+ N) {K : add_subgroup G} {x : G} (hx : x K) :
theorem subgroup.mem_map_of_mem {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) {K : subgroup G} {x : G} (hx : x K) :
theorem add_subgroup.apply_coe_mem_map {G : Type u_1} [add_group G] {N : Type u_4} [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_4} [group N] (f : G →* N) (K : subgroup G) (x : K) :
theorem add_subgroup.map_mono {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {K K' : add_subgroup G} :
theorem subgroup.map_mono {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {K K' : subgroup G} :
@[simp]
@[simp]
theorem subgroup.map_id {G : Type u_1} [group G] (K : subgroup G) :
theorem add_subgroup.map_map {G : Type u_1} [add_group G] (K : add_subgroup G) {N : Type u_4} [add_group N] {P : Type u_5} [add_group P] (g : N →+ P) (f : G →+ N) :
theorem subgroup.map_map {G : Type u_1} [group G] (K : subgroup G) {N : Type u_4} [group N] {P : Type u_5} [group P] (g : N →* P) (f : G →* N) :
@[simp]
theorem subgroup.map_one_eq_bot {G : Type u_1} [group G] (K : subgroup G) {N : Type u_4} [group N] :
@[simp]
theorem add_subgroup.map_zero_eq_bot {G : Type u_1} [add_group G] (K : add_subgroup G) {N : Type u_4} [add_group N] :
theorem subgroup.mem_map_equiv {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G ≃* N} {K : subgroup G} {x : N} :
theorem add_subgroup.mem_map_equiv {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G ≃+ N} {K : add_subgroup G} {x : N} :
theorem subgroup.mem_map_iff_mem {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} (hf : function.injective f) {K : subgroup G} {x : G} :
theorem add_subgroup.mem_map_iff_mem {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} (hf : function.injective f) {K : add_subgroup G} {x : G} :
theorem subgroup.map_symm_eq_iff_map_eq {G : Type u_1} [group G] (K : subgroup G) {N : Type u_4} [group N] {H : subgroup N} {e : G ≃* N} :
theorem add_subgroup.map_symm_eq_iff_map_eq {G : Type u_1} [add_group G] (K : add_subgroup G) {N : Type u_4} [add_group N] {H : add_subgroup N} {e : G ≃+ N} :
theorem add_subgroup.map_le_iff_le_comap {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {K : add_subgroup G} {H : add_subgroup N} :
theorem subgroup.map_le_iff_le_comap {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {K : subgroup G} {H : subgroup N} :
theorem subgroup.gc_map_comap {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
theorem add_subgroup.map_sup {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H K : add_subgroup G) (f : G →+ N) :
theorem subgroup.map_sup {G : Type u_1} [group G] {N : Type u_4} [group N] (H K : subgroup G) (f : G →* N) :
theorem add_subgroup.map_supr {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι add_subgroup G) :
theorem subgroup.map_supr {G : Type u_1} [group G] {N : Type u_4} [group N] {ι : Sort u_2} (f : G →* N) (s : ι subgroup G) :
subgroup.map f (supr s) = (i : ι), subgroup.map f (s i)
theorem subgroup.comap_sup_comap_le {G : Type u_1} [group G] {N : Type u_4} [group N] (H K : subgroup N) (f : G →* N) :
theorem add_subgroup.supr_comap_le {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι add_subgroup N) :
theorem subgroup.supr_comap_le {G : Type u_1} [group G] {N : Type u_4} [group N] {ι : Sort u_2} (f : G →* N) (s : ι subgroup N) :
( (i : ι), subgroup.comap f (s i)) subgroup.comap f (supr s)
theorem add_subgroup.comap_inf {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H K : add_subgroup N) (f : G →+ N) :
theorem subgroup.comap_inf {G : Type u_1} [group G] {N : Type u_4} [group N] (H K : subgroup N) (f : G →* N) :
theorem subgroup.comap_infi {G : Type u_1} [group G] {N : Type u_4} [group N] {ι : Sort u_2} (f : G →* N) (s : ι subgroup N) :
subgroup.comap f (infi s) = (i : ι), subgroup.comap f (s i)
theorem add_subgroup.comap_infi {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι add_subgroup N) :
theorem add_subgroup.map_inf_le {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H K : add_subgroup G) (f : G →+ N) :
theorem subgroup.map_inf_le {G : Type u_1} [group G] {N : Type u_4} [group N] (H K : subgroup G) (f : G →* N) :
theorem subgroup.map_inf_eq {G : Type u_1} [group G] {N : Type u_4} [group N] (H K : subgroup G) (f : G →* N) (hf : function.injective f) :
theorem add_subgroup.map_inf_eq {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H K : add_subgroup G) (f : G →+ N) (hf : function.injective f) :
@[simp]
theorem add_subgroup.map_bot {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :
@[simp]
theorem subgroup.map_bot {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
@[simp]
theorem subgroup.map_top_of_surjective {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (h : function.surjective f) :
@[simp]
@[simp]
theorem subgroup.comap_top {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
@[simp]
theorem add_subgroup.comap_top {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :
def subgroup.subgroup_of {G : Type u_1} [group G] (H K : subgroup G) :

For any subgroups H and K, view H ⊓ K as a subgroup of K.

Equations
Instances for subgroup.subgroup_of
@[simp]
def subgroup.subgroup_of_equiv_of_le {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :

If H ≤ K, then H as a subgroup of K is isomorphic to H.

Equations

If H ≤ K, then H as a subgroup of K is isomorphic to H.

Equations
@[simp]
theorem subgroup.comap_subtype {G : Type u_1} [group G] (H K : subgroup G) :
@[simp]
theorem subgroup.comap_inclusion_subgroup_of {G : Type u_1} [group G] {K₁ K₂ : subgroup G} (h : K₁ K₂) (H : subgroup G) :
theorem subgroup.coe_subgroup_of {G : Type u_1} [group G] (H K : subgroup G) :
theorem subgroup.mem_subgroup_of {G : Type u_1} [group G] {H K : subgroup G} {h : K} :
theorem add_subgroup.mem_add_subgroup_of {G : Type u_1} [add_group G] {H K : add_subgroup G} {h : K} :
@[simp]
theorem subgroup.subgroup_of_map_subtype {G : Type u_1} [group G] (H K : subgroup G) :
@[simp]
theorem subgroup.bot_subgroup_of {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem subgroup.top_subgroup_of {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem subgroup.subgroup_of_self {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem add_subgroup.add_subgroup_of_inj {G : Type u_1} [add_group G] {H₁ H₂ K : add_subgroup G} :
H₁.add_subgroup_of K = H₂.add_subgroup_of K H₁ K = H₂ K
@[simp]
theorem subgroup.subgroup_of_inj {G : Type u_1} [group G] {H₁ H₂ K : subgroup G} :
H₁.subgroup_of K = H₂.subgroup_of K H₁ K = H₂ K
@[simp]
theorem subgroup.inf_subgroup_of_right {G : Type u_1} [group G] (H K : subgroup G) :
@[simp]
theorem subgroup.inf_subgroup_of_left {G : Type u_1} [group G] (H K : subgroup G) :
@[simp]
theorem subgroup.subgroup_of_eq_bot {G : Type u_1} [group G] {H K : subgroup G} :
@[simp]
@[simp]
theorem subgroup.subgroup_of_eq_top {G : Type u_1} [group G] {H K : subgroup G} :
def add_subgroup.prod {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :

Given add_subgroups H, K of add_groups A, B respectively, H × K as an add_subgroup of A × B.

Equations
Instances for add_subgroup.prod
def subgroup.prod {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) (K : subgroup N) :
subgroup (G × N)

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

Equations
Instances for subgroup.prod
theorem subgroup.coe_prod {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) (K : subgroup N) :
(H.prod K) = H ×ˢ K
theorem add_subgroup.coe_prod {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :
(H.prod K) = H ×ˢ K
theorem add_subgroup.mem_prod {G : Type u_1} [add_group G] {N : Type u_4} [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_4} [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_right {G : Type u_1} [group G] {N : Type u_4} [group N] (K : subgroup G) :
monotone (λ (t : subgroup N), K.prod t)
theorem add_subgroup.prod_mono_right {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (K : add_subgroup G) :
monotone (λ (t : add_subgroup N), K.prod t)
theorem add_subgroup.prod_mono_left {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup N) :
monotone (λ (K : add_subgroup G), K.prod H)
theorem subgroup.prod_mono_left {G : Type u_1} [group G] {N : Type u_4} [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_4} [group N] (K : subgroup G) :
theorem subgroup.top_prod {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup N) :
@[simp]
theorem subgroup.top_prod_top {G : Type u_1} [group G] {N : Type u_4} [group N] :
@[simp]
theorem add_subgroup.top_prod_top {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] :
theorem subgroup.bot_prod_bot {G : Type u_1} [group G] {N : Type u_4} [group N] :
theorem add_subgroup.bot_sum_bot {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] :
theorem subgroup.le_prod_iff {G : Type u_1} [group G] {N : Type u_4} [group N] {H : subgroup G} {K : subgroup N} {J : subgroup (G × N)} :
theorem subgroup.prod_le_iff {G : Type u_1} [group G] {N : Type u_4} [group N] {H : subgroup G} {K : subgroup N} {J : subgroup (G × N)} :
@[simp]
theorem subgroup.prod_eq_bot_iff {G : Type u_1} [group G] {N : Type u_4} [group N] {H : subgroup G} {K : subgroup N} :
H.prod K = H = K =
@[simp]
theorem add_subgroup.prod_eq_bot_iff {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {H : add_subgroup G} {K : add_subgroup N} :
H.prod K = H = K =
def subgroup.prod_equiv {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) (K : subgroup N) :

Product of subgroups is isomorphic to their product as groups.

Equations
def add_subgroup.prod_equiv {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :

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

Equations
def add_submonoid.pi {η : Type u_6} {f : η Type u_7} [Π (i : η), add_zero_class (f i)] (I : set η) (s : Π (i : η), add_submonoid (f i)) :
add_submonoid (Π (i : η), f i)

A version of set.pi for add_submonoids. Given an index set I and a family of submodules s : Π i, add_submonoid f i, pi I s is the add_submonoid of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I. -/

Equations
def submonoid.pi {η : Type u_6} {f : η Type u_7} [Π (i : η), mul_one_class (f i)] (I : set η) (s : Π (i : η), submonoid (f i)) :
submonoid (Π (i : η), f i)

A version of set.pi for submonoids. Given an index set I and a family of submodules s : Π i, submonoid f i, pi I s is the submonoid of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

Equations
def add_subgroup.pi {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] (I : set η) (H : Π (i : η), add_subgroup (f i)) :
add_subgroup (Π (i : η), f i)

A version of set.pi for add_subgroups. Given an index set I and a family of submodules s : Π i, add_subgroup f i, pi I s is the add_subgroup of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I. -/

Equations
def subgroup.pi {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] (I : set η) (H : Π (i : η), subgroup (f i)) :
subgroup (Π (i : η), f i)

A version of set.pi for subgroups. Given an index set I and a family of submodules s : Π i, subgroup f i, pi I s is the subgroup of dependent functions f : Π i, f i such that f i belongs to pi I s whenever i ∈ I.

Equations
theorem add_subgroup.coe_pi {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] (I : set η) (H : Π (i : η), add_subgroup (f i)) :
(add_subgroup.pi I H) = I.pi (λ (i : η), (H i))
theorem subgroup.coe_pi {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] (I : set η) (H : Π (i : η), subgroup (f i)) :
(subgroup.pi I H) = I.pi (λ (i : η), (H i))
theorem add_subgroup.mem_pi {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] (I : set η) {H : Π (i : η), add_subgroup (f i)} {p : Π (i : η), f i} :
p add_subgroup.pi I H (i : η), i I p i H i
theorem subgroup.mem_pi {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] (I : set η) {H : Π (i : η), subgroup (f i)} {p : Π (i : η), f i} :
p subgroup.pi I H (i : η), i I p i H i
theorem subgroup.pi_top {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] (I : set η) :
subgroup.pi I (λ (i : η), ) =
theorem add_subgroup.pi_top {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] (I : set η) :
add_subgroup.pi I (λ (i : η), ) =
theorem add_subgroup.pi_empty {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] (H : Π (i : η), add_subgroup (f i)) :
theorem subgroup.pi_empty {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] (H : Π (i : η), subgroup (f i)) :
theorem add_subgroup.pi_bot {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] :
theorem subgroup.pi_bot {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] :
subgroup.pi set.univ (λ (i : η), ) =
theorem add_subgroup.le_pi_iff {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] {I : set η} {H : Π (i : η), add_subgroup (f i)} {J : add_subgroup (Π (i : η), f i)} :
theorem subgroup.le_pi_iff {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] {I : set η} {H : Π (i : η), subgroup (f i)} {J : subgroup (Π (i : η), f i)} :
J subgroup.pi I H (i : η), i I subgroup.map (pi.eval_monoid_hom f i) J H i
@[simp]
theorem subgroup.mul_single_mem_pi {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] [decidable_eq η] {I : set η} {H : Π (i : η), subgroup (f i)} (i : η) (x : f i) :
@[simp]
theorem add_subgroup.single_mem_pi {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] [decidable_eq η] {I : set η} {H : Π (i : η), add_subgroup (f i)} (i : η) (x : f i) :
theorem subgroup.pi_eq_bot_iff {η : Type u_6} {f : η Type u_7} [Π (i : η), group (f i)] (H : Π (i : η), subgroup (f i)) :
subgroup.pi set.univ H = (i : η), H i =
theorem add_subgroup.pi_eq_bot_iff {η : Type u_6} {f : η Type u_7} [Π (i : η), add_group (f i)] (H : Π (i : η), add_subgroup (f i)) :
@[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
@[class]
structure subgroup.characteristic {G : Type u_1} [group G] (H : subgroup G) :
Prop

A subgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form characteristic.iff...

Instances of this typeclass
@[protected, instance]
@[class]
structure add_subgroup.characteristic {A : Type u_3} [add_group A] (H : add_subgroup A) :
Prop

A add_subgroup is characteristic if it is fixed by all automorphisms. Several equivalent conditions are provided by lemmas of the form characteristic.iff...

Instances of this typeclass
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

The center of an additive group G is the set of elements that commute with everything in G

Equations
Instances for add_subgroup.center
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
Instances for subgroup.center
Instances for subgroup.center
theorem subgroup.mem_center_iff {G : Type u_1} [group G] {z : G} :
z subgroup.center G (g : G), g * z = z * g
theorem add_subgroup.mem_center_iff {G : Type u_1} [add_group G] {z : G} :
z add_subgroup.center G (g : G), g + z = z + g
@[protected, instance]
def subgroup.decidable_mem_center {G : Type u_1} [group G] (z : G) [decidable ( (g : G), g * z = z * g)] :
Equations
@[protected, instance]

A group is commutative if the center is the whole group

Equations

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

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

Equations
theorem add_subgroup.mem_normalizer_iff {G : Type u_1} [add_group G] {H : add_subgroup G} {g : G} :
g H.normalizer (h : G), h H g + h + -g H
theorem subgroup.mem_normalizer_iff {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g H.normalizer (h : G), h H g * h * g⁻¹ H
theorem add_subgroup.mem_normalizer_iff'' {G : Type u_1} [add_group G] {H : add_subgroup G} {g : G} :
g H.normalizer (h : G), h H -g + h + g H
theorem subgroup.mem_normalizer_iff'' {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g H.normalizer (h : G), h H g⁻¹ * h * g H
theorem subgroup.mem_normalizer_iff' {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g H.normalizer (n : G), n * g H g * n H
theorem add_subgroup.mem_normalizer_iff' {G : Type u_1} [add_group G] {H : add_subgroup G} {g : G} :
g H.normalizer (n : G), n + g H g + n H
theorem subgroup.le_normalizer {G : Type u_1} [group G] {H : subgroup G} :
@[protected, instance]
@[protected, instance]
theorem subgroup.normalizer_eq_top {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.subgroup_of K).normal] (HK : H K) :
theorem add_subgroup.le_normalizer_of_normal {G : Type u_1} [add_group G] {H K : add_subgroup G} [hK : (H.add_subgroup_of K).normal] (HK : H K) :
theorem subgroup.le_normalizer_comap {G : Type u_1} [group G] {H : subgroup G} {N : Type u_4} [group N] (f : N →* G) :

The preimage of the normalizer is contained in the normalizer of the preimage.

The preimage of the normalizer is contained in the normalizer of the preimage.

theorem subgroup.le_normalizer_map {G : Type u_1} [group G] {H : subgroup G} {N : Type u_4} [group N] (f : G →* N) :

The image of the normalizer is contained in the normalizer of the image.

The image of the normalizer is contained in the normalizer of the image.

def normalizer_condition (G : Type u_1) [group G] :
Prop

Every proper subgroup H of G is a proper normal subgroup of the normalizer of H in G.

Equations

Alternative phrasing of the normalizer condition: Only the full group is self-normalizing. This may be easier to work with, as it avoids inequalities and negations.

In a group that satisifes the normalizer condition, every maximal subgroup is normal

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

The centralizer of H is the subgroup of g : G commuting with every h : H.

Equations
Instances for subgroup.centralizer

The centralizer of H is the additive subgroup of g : G commuting with every h : H.

Equations
Instances for add_subgroup.centralizer
theorem add_subgroup.mem_centralizer_iff {G : Type u_1} [add_group G] {H : add_subgroup G} {g : G} :
g H.centralizer (h : G), h H h + g = g + h
theorem subgroup.mem_centralizer_iff {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g H.centralizer (h : G), h H h * g = g * h
theorem subgroup.mem_centralizer_iff_commutator_eq_one {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g H.centralizer (h : G), h H h * g * h⁻¹ * g⁻¹ = 1
theorem add_subgroup.mem_centralizer_iff_commutator_eq_zero {G : Type u_1} [add_group G] {H : add_subgroup G} {g : G} :
g H.centralizer (h : G), h H h + g + -h + -g = 0
theorem subgroup.le_centralizer_iff {G : Type u_1} [group G] {H K : subgroup G} :
theorem add_subgroup.centralizer_le {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :
theorem subgroup.centralizer_le {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :
@[protected, instance]
@[class]
structure add_subgroup.is_commutative {A : Type u_3} [add_group A] (H : add_subgroup A) :
Prop

Commutivity of an additive subgroup

Instances of this typeclass
@[protected, instance]

A commutative subgroup is commutative.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def subgroup.map_is_commutative {G : Type u_1} {G' : Type u_2} [group G] [group G'] (H : subgroup G) (f : G →* G') [H.is_commutative] :
theorem subgroup.comap_injective_is_commutative {G : Type u_1} {G' : Type u_2} [group G] [group G'] (H : subgroup G) {f : G' →* G} (hf : function.injective f) [H.is_commutative] :
@[protected, instance]
theorem subgroup.le_centralizer {G : Type u_1} [group G] (H : subgroup G) [h : H.is_commutative] :
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
theorem group.mem_conjugates_of_set_iff {G : Type u_1} [group G] {s : set G} {x : G} :
x group.conjugates_of_set s (a : G) (H : a s), is_conj a x
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) :

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
Instances for subgroup.normal_closure
@[protected, instance]

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_eq_infi {G : Type u_1} [group G] {s : set G} :
subgroup.normal_closure s = (N : subgroup G) (_x : N.normal) (hs : s N), N
@[simp]
def subgroup.normal_core {G : Type u_1} [group G] (H : subgroup G) :

The normal core of a subgroup H is the largest normal subgroup of G contained in H, as shown by subgroup.normal_core_eq_supr.

Equations
Instances for subgroup.normal_core
theorem subgroup.normal_core_le {G : Type u_1} [group G] (H : subgroup G) :
@[protected, instance]
theorem subgroup.normal_le_normal_core {G : Type u_1} [group G] {H N : subgroup G} [hN : N.normal] :
theorem subgroup.normal_core_mono {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :
theorem subgroup.normal_core_eq_supr {G : Type u_1} [group G] (H : subgroup G) :
H.normal_core = (N : subgroup G) (_x : N.normal) (hs : N H), N
@[simp]
theorem subgroup.normal_core_eq_self {G : Type u_1} [group G] (H : subgroup G) [H.normal] :
def add_monoid_hom.range {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :

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

Equations
Instances for add_monoid_hom.range
def monoid_hom.range {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :

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

Equations
Instances for monoid_hom.range
@[simp]
theorem add_monoid_hom.coe_range {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :
@[simp]
theorem monoid_hom.coe_range {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
@[simp]
theorem monoid_hom.mem_range {G : Type u_1} [group G] {N : Type u_4} [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_4} [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_4} [group N] (f : G →* N) :
theorem add_monoid_hom.range_eq_map {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :
@[simp]
theorem monoid_hom.restrict_range {G : Type u_1} [group G] {N : Type u_4} [group N] (K : subgroup G) (f : G →* N) :
@[simp]
theorem add_monoid_hom.restrict_range {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (K : add_subgroup G) (f : G →+ N) :
def monoid_hom.range_restrict {G : Type u_1} [group G] {N : Type u_4} [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_4} [add_group N] (f : G →+ N) :

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

Equations
@[simp]
theorem monoid_hom.coe_range_restrict {G : Type u_1} [group G] {N : Type u_4} [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_4} [add_group N] (f : G →+ N) (g : G) :
theorem monoid_hom.coe_comp_range_restrict {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
theorem monoid_hom.subtype_comp_range_restrict {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
theorem monoid_hom.map_range {G : Type u_1} [group G] {N : Type u_4} {P : Type u_5} [group N] [group P] (g : N →* P) (f : G →* N) :
theorem add_monoid_hom.map_range {G : Type u_1} [add_group G] {N : Type u_4} {P : Type u_5} [add_group N] [add_group P] (g : N →+ P) (f : G →+ N) :
theorem monoid_hom.range_top_iff_surjective {G : Type u_1} [group G] {N : Type u_2} [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]
theorem monoid_hom.range_one {G : Type u_1} [group G] {N : Type u_4} [group N] :
@[simp]
theorem add_monoid_hom.range_zero {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] :
@[simp]
theorem add_subgroup.subtype_range {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp]
theorem subgroup.subtype_range {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem add_subgroup.inclusion_range {G : Type u_1} [add_group G] {H K : add_subgroup G} (h_le : H K) :
@[simp]
theorem subgroup.inclusion_range {G : Type u_1} [group G] {H K : subgroup G} (h_le : H K) :
theorem monoid_hom.subgroup_of_range_eq_of_le {G₁ : Type u_1} {G₂ : Type u_2} [group G₁] [group G₂] {K : subgroup G₂} (f : G₁ →* G₂) (h : f.range K) :
theorem add_monoid_hom.add_subgroup_of_range_eq_of_le {G₁ : Type u_1} {G₂ : Type u_2} [add_group G₁] [add_group G₂] {K : add_subgroup G₂} (f : G₁ →+ G₂) (h : f.range K) :
def monoid_hom.of_left_inverse {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {g : N →* G} (h : function.left_inverse g f) :

Computable alternative to monoid_hom.of_injective.

Equations
def add_monoid_hom.of_left_inverse {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {g : N →+ G} (h : function.left_inverse g f) :

Computable alternative to add_monoid_hom.of_injective.

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

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

Equations
noncomputable def add_monoid_hom.of_injective {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} (hf : function.injective f) :

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

Equations
theorem monoid_hom.of_injective_apply {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} (hf : function.injective f) {x : G} :
theorem add_monoid_hom.of_injective_apply {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} (hf : function.injective f) {x : G} :
def monoid_hom.ker {G : Type u_1} [group G] {M : Type u_6} [mul_one_class M] (f : G →* M) :

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

Equations
Instances for monoid_hom.ker
def add_monoid_hom.ker {G : Type u_1} [add_group G] {M : Type u_6} [add_zero_class M] (f : G →+ M) :

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

Equations
Instances for add_monoid_hom.ker
theorem monoid_hom.mem_ker {G : Type u_1} [group G] {M : Type u_6} [mul_one_class M] (f : G →* M) {x : G} :
x f.ker f x = 1
theorem add_monoid_hom.mem_ker {G : Type u_1} [add_group G] {M : Type u_6} [add_zero_class M] (f : G →+ M) {x : G} :
x f.ker f x = 0
theorem add_monoid_hom.coe_ker {G : Type u_1} [add_group G] {M : Type u_6} [add_zero_class M] (f : G →+ M) :
(f.ker) = f ⁻¹' {0}
theorem monoid_hom.coe_ker {G : Type u_1} [group G] {M : Type u_6} [mul_one_class M] (f : G →* M) :
(f.ker) = f ⁻¹' {1}
@[simp]
theorem add_monoid_hom.ker_to_hom_add_units {G : Type u_1} [add_group G] {M : Type u_2} [add_monoid M] (f : G →+ M) :
@[simp]
theorem monoid_hom.ker_to_hom_units {G : Type u_1} [group G] {M : Type u_2} [monoid M] (f : G →* M) :
theorem add_monoid_hom.eq_iff {G : Type u_1} [add_group G] {M : Type u_6} [add_zero_class M] (f : G →+ M) {x y : G} :
f x = f y -y + x f.ker
theorem monoid_hom.eq_iff {G : Type u_1} [group G] {M : Type u_6} [mul_one_class M] (f : G →* M) {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] {M : Type u_6} [mul_one_class M] [decidable_eq M] (f : G →* M) :
decidable_pred (λ (_x : G), _x f.ker)
Equations
@[protected, instance]
def add_monoid_hom.decidable_mem_ker {G : Type u_1} [add_group G] {M : Type u_6} [add_zero_class M] [decidable_eq M] (f : G →+ M) :
decidable_pred (λ (_x : G), _x f.ker)
Equations
theorem add_monoid_hom.comap_ker {G : Type u_1} [add_group G] {N : Type u_4} {P : Type u_5} [add_group N] [add_group P] (g : N →+ P) (f : G →+ N) :
theorem monoid_hom.comap_ker {G : Type u_1} [group G] {N : Type u_4} {P : Type u_5} [group N] [group P] (g : N →* P) (f : G →* N) :
@[simp]
theorem monoid_hom.comap_bot {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
@[simp]
theorem add_monoid_hom.comap_bot {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :
@[simp]
theorem monoid_hom.ker_restrict {G : Type u_1} [group G] {N : Type u_4} [group N] (K : subgroup G) (f : G →* N) :
@[simp]
theorem add_monoid_hom.ker_restrict {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (K : add_subgroup G) (f : G →+ N) :
@[simp]
theorem add_monoid_hom.ker_cod_restrict {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {S : Type u_2} [set_like S N] [add_submonoid_class S N] (f : G →+ N) (s : S) (h : (x : G), f x s) :
(f.cod_restrict s h).ker = f.ker
@[simp]
theorem monoid_hom.ker_cod_restrict {G : Type u_1} [group G] {N : Type u_4} [group N] {S : Type u_2} [set_like S N] [submonoid_class S N] (f : G →* N) (s : S) (h : (x : G), f x s) :
(f.cod_restrict s h).ker = f.ker
@[simp]
theorem monoid_hom.ker_range_restrict {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
@[simp]
theorem add_monoid_hom.ker_range_restrict {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :
@[simp]
theorem monoid_hom.ker_one {G : Type u_1} [group G] {M : Type u_6} [mul_one_class M] :
@[simp]
theorem add_monoid_hom.ker_zero {G : Type u_1} [add_group G] {M : Type u_6} [add_zero_class M] :
@[simp]
theorem monoid_hom.ker_id {G : Type u_1} [group G] :
@[simp]
theorem monoid_hom.ker_eq_bot_iff {G : Type u_1} [group G] {M : Type u_6} [mul_one_class M] (f : G →* M) :
@[simp]
theorem subgroup.ker_subtype {G : Type u_1} [group G] (H : subgroup G) :
@[simp]
theorem add_subgroup.ker_subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :
@[simp]
theorem subgroup.ker_inclusion {G : Type u_1} [group G] {H K : subgroup G} (h : H K) :
@[simp]
theorem add_subgroup.ker_inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H K) :
theorem add_monoid_hom.sum_map_comap_sum {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {G' : Type u_2} {N' : Type u_3} [add_group G'] [add_group N'] (f : G →+ N) (g : G' →+ N') (S : add_subgroup N) (S' : add_subgroup N') :
theorem monoid_hom.prod_map_comap_prod {G : Type u_1} [group G] {N : Type u_4} [group N] {G' : Type u_2} {N' : Type u_3} [group G'] [group N'] (f : G →* N) (g : G' →* N') (S : subgroup N) (S' : subgroup N') :
theorem monoid_hom.ker_prod_map {G : Type u_1} [group G] {N : Type u_4} [group N] {G' : Type u_2} {N' : Type u_3} [group G'] [group N'] (f : G →* N) (g : G' →* N') :
(f.prod_map g).ker = f.ker.prod g.ker
theorem add_monoid_hom.ker_sum_map {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {G' : Type u_2} {N' : Type u_3} [add_group G'] [add_group N'] (f : G →+ N) (g : G' →+ N') :
(f.prod_map g).ker = f.ker.prod g.ker
@[protected, instance]
def monoid_hom.normal_ker {G : Type u_1} [group G] {M : Type u_6} [mul_one_class M] (f : G →* M) :
@[protected, instance]
def add_monoid_hom.normal_ker {G : Type u_1} [add_group G] {M : Type u_6} [add_zero_class M] (f : G →+ M) :
def monoid_hom.eq_locus {G : Type u_1} [group G] {M : Type u_6} [monoid M] (f g : G →* M) :

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] {M : Type u_6} [add_monoid M] (f g : G →+ M) :

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

Equations
@[simp]
theorem add_monoid_hom.eq_locus_same {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) :
@[simp]
theorem monoid_hom.eq_locus_same {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) :
theorem add_monoid_hom.eq_on_closure {G : Type u_1} [add_group G] {M : Type u_6} [add_monoid M] {f g : G →+ M} {s : set G} (h : set.eq_on f g s) :

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

theorem monoid_hom.eq_on_closure {G : Type u_1} [group G] {M : Type u_6} [monoid M] {f g : G →* M} {s : set G} (h : set.eq_on f g s) :

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] {M : Type u_6} [add_monoid M] {f g : G →+ M} (h : set.eq_on f g ) :
f = g
theorem monoid_hom.eq_of_eq_on_top {G : Type u_1} [group G] {M : Type u_6} [monoid M] {f g : G →* M} (h : set.eq_on f g ) :
f = g
theorem add_monoid_hom.eq_of_eq_on_dense {G : Type u_1} [add_group G] {M : Type u_6} [add_monoid M] {s : set G} (hs : add_subgroup.closure s = ) {f g : G →+ M} (h : set.eq_on f g s) :
f = g
theorem monoid_hom.eq_of_eq_on_dense {G : Type u_1} [group G] {M : Type u_6} [monoid M] {s : set G} (hs : subgroup.closure s = ) {f g : G →* M} (h : set.eq_on f g s) :
f = g
theorem monoid_hom.closure_preimage_le {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (s : set N) :
theorem add_monoid_hom.map_closure {G : Type u_1} [add_group G] {N : Type u_4} [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_4} [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.normal.map {G : Type u_1} [group G] {N : Type u_4} [group N] {H : subgroup G} (h : H.normal) (f : G →* N) (hf : function.surjective f) :
theorem add_subgroup.normal.map {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {H : add_subgroup G} (h : H.normal) (f : G →+ N) (hf : function.surjective f) :
theorem subgroup.map_eq_bot_iff {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) {f : G →* N} :
theorem add_subgroup.map_eq_bot_iff {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup G) {f : G →+ N} :
theorem subgroup.map_eq_bot_iff_of_injective {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) {f : G →* N} (hf : function.injective f) :
theorem add_subgroup.map_le_range {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) (H : add_subgroup G) :
theorem subgroup.map_le_range {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H : subgroup G) :
theorem subgroup.map_subtype_le {G : Type u_1} [group G] {H : subgroup G} (K : subgroup H) :
theorem subgroup.ker_le_comap {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H : subgroup N) :
theorem add_subgroup.ker_le_comap {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) (H : add_subgroup N) :
theorem add_subgroup.map_comap_le {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) (H : add_subgroup N) :
theorem subgroup.map_comap_le {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H : subgroup N) :
theorem subgroup.le_comap_map {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H : subgroup G) :
theorem add_subgroup.le_comap_map {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) (H : add_subgroup G) :
theorem add_subgroup.map_comap_eq {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) (H : add_subgroup N) :
theorem subgroup.map_comap_eq {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H : subgroup N) :
theorem add_subgroup.comap_map_eq {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) (H : add_subgroup G) :
theorem subgroup.comap_map_eq {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H : subgroup G) :
theorem add_subgroup.map_comap_eq_self {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {H : add_subgroup N} (h : H f.range) :
theorem subgroup.map_comap_eq_self {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {H : subgroup N} (h : H f.range) :
theorem subgroup.map_comap_eq_self_of_surjective {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} (h : function.surjective f) (H : subgroup N) :
theorem subgroup.comap_le_comap_of_le_range {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {K L : subgroup N} (hf : K f.range) :
theorem add_subgroup.comap_le_comap_of_le_range {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {K L : add_subgroup N} (hf : K f.range) :
theorem subgroup.comap_le_comap_of_surjective {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {K L : subgroup N} (hf : function.surjective f) :
theorem subgroup.comap_lt_comap_of_surjective {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {K L : subgroup N} (hf : function.surjective f) :
theorem subgroup.comap_injective {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} (h : function.surjective f) :
theorem subgroup.comap_map_eq_self {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {H : subgroup G} (h : f.ker H) :
theorem add_subgroup.comap_map_eq_self {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {H : add_subgroup G} (h : f.ker H) :
theorem subgroup.comap_map_eq_self_of_injective {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} (h : function.injective f) (H : subgroup G) :
theorem add_subgroup.map_le_map_iff {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {H K : add_subgroup G} :
theorem subgroup.map_le_map_iff {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {H K : subgroup G} :
theorem add_subgroup.map_le_map_iff' {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {H K : add_subgroup G} :
theorem subgroup.map_le_map_iff' {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {H K : subgroup G} :
theorem add_subgroup.map_eq_map_iff {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {H K : add_subgroup G} :
theorem subgroup.map_eq_map_iff {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {H K : subgroup G} :
theorem subgroup.map_eq_range_iff {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {H : subgroup G} :
theorem add_subgroup.map_eq_range_iff {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {f : G →+ N} {H : add_subgroup G} :
theorem subgroup.map_le_map_iff_of_injective {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} (hf : function.injective f) {H K : subgroup G} :
@[simp]
theorem subgroup.map_injective {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} (h : function.injective f) :
theorem subgroup.map_eq_comap_of_inverse {G : Type u_1} [group G] {N : Type u_4} [group N] {f : G →* N} {g : N →* G} (hl : function.left_inverse g f) (hr : function.right_inverse g f) (H : subgroup G) :
theorem add_subgroup.map_injective_of_ker_le {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) {H K : add_subgroup G} (hH : f.ker H) (hK : f.ker K) (hf : add_subgroup.map f H = add_subgroup.map f K) :
H = K

Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

theorem subgroup.map_injective_of_ker_le {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) {H K : subgroup G} (hH : f.ker H) (hK : f.ker K) (hf : subgroup.map f H = subgroup.map f K) :
H = K

Given f(A) = f(B), ker f ≤ A, and ker f ≤ B, deduce that A = B.

theorem subgroup.comap_sup_eq_of_le_range {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) {H K : subgroup N} (hH : H f.range) (hK : K f.range) :
theorem add_subgroup.comap_sup_eq_of_le_range {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (f : G →+ N) {H K : add_subgroup N} (hH : H f.range) (hK : K f.range) :
theorem subgroup.comap_sup_eq {G : Type u_1} [group G] {N : Type u_4} [group N] (f : G →* N) (H K : subgroup N) (hf : function.surjective f) :
theorem subgroup.sup_subgroup_of_eq {G : Type u_1} [group G] {H K L : subgroup G} (hH : H L) (hK : K L) :
theorem add_subgroup.sup_add_subgroup_of_eq {G : Type u_1} [add_group G] {H K L : add_subgroup G} (hH : H L) (hK : K L) :
theorem subgroup.codisjoint_subgroup_of_sup {G : Type u_1} [group G] (H K : subgroup G) :
noncomputable def subgroup.equiv_map_of_injective {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) (f : G →* N) (hf : function.injective f) :

A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use mul_equiv.subgroup_map for better definitional equalities.

Equations
noncomputable def add_subgroup.equiv_map_of_injective {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup G) (f : G →+ N) (hf : function.injective f) :

An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use add_equiv.add_subgroup_map for better definitional equalities.

Equations
@[simp]
theorem subgroup.coe_equiv_map_of_injective_apply {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) (f : G →* N) (hf : function.injective f) (h : H) :
@[simp]
theorem add_subgroup.coe_equiv_map_of_injective_apply {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup G) (f : G →+ N) (hf : function.injective f) (h : H) :

The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.

The preimage of the normalizer is equal to the normalizer of the preimage of a surjective function.

The image of the normalizer is equal to the normalizer of the image of an isomorphism.

The image of the normalizer is equal to the normalizer of the image of an isomorphism.

theorem subgroup.map_normalizer_eq_of_bijective {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) {f : G →* N} (hf : function.bijective f) :

The image of the normalizer is equal to the normalizer of the image of a bijective function.

The image of the normalizer is equal to the normalizer of the image of a bijective function.

def add_monoid_hom.lift_of_right_inverse_aux {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) (g : G₁ →+ G₃) (hg : f.ker g.ker) :
G₂ →+ G₃

Auxiliary definition used to define lift_of_right_inverse

Equations
def monoid_hom.lift_of_right_inverse_aux {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv 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_4} {G₂ : Type u_5} {G₃ : Type u_6} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv 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_4} {G₂ : Type u_5} {G₃ : Type u_6} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv 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_4} {G₂ : Type u_5} {G₃ : Type u_6} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) :
{g // f.ker g.ker} (G₂ →+ G₃)

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

See add_monoid_hom.eq_lift_of_right_inverse for the uniqueness lemma.

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

lift_of_right_inverse f hf g hg is the unique group homomorphism φ

See monoid_hom.eq_lift_of_right_inverse for the uniqueness lemma.

   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ
Equations
@[simp, reducible]
noncomputable def add_monoid_hom.lift_of_surjective {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [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.

@[simp, reducible]
noncomputable def monoid_hom.lift_of_surjective {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (hf : function.surjective f) :
{g // f.ker g.ker} (G₂ →* G₃)

A non-computable version of monoid_hom.lift_of_right_inverse for when no computable right inverse is available, that uses function.surj_inv.

@[simp]
theorem monoid_hom.lift_of_right_inverse_comp_apply {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) (g : {g // f.ker g.ker}) (x : G₁) :
((f.lift_of_right_inverse f_inv hf) g) (f x) = g x
@[simp]
theorem add_monoid_hom.lift_of_right_inverse_comp_apply {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) (g : {g // f.ker g.ker}) (x : G₁) :
((f.lift_of_right_inverse f_inv hf) g) (f x) = g x
@[simp]
theorem add_monoid_hom.lift_of_right_inverse_comp {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) (g : {g // f.ker g.ker}) :
((f.lift_of_right_inverse f_inv hf) g).comp f = g
@[simp]
theorem monoid_hom.lift_of_right_inverse_comp {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) (g : {g // f.ker g.ker}) :
((f.lift_of_right_inverse f_inv hf) g).comp f = g
theorem add_monoid_hom.eq_lift_of_right_inverse {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [add_group G₁] [add_group G₂] [add_group G₃] (f : G₁ →+ G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) (g : G₁ →+ G₃) (hg : f.ker g.ker) (h : G₂ →+ G₃) (hh : h.comp f = g) :
h = (f.lift_of_right_inverse f_inv hf) g, hg⟩
theorem monoid_hom.eq_lift_of_right_inverse {G₁ : Type u_4} {G₂ : Type u_5} {G₃ : Type u_6} [group G₁] [group G₂] [group G₃] (f : G₁ →* G₂) (f_inv : G₂ G₁) (hf : function.right_inverse f_inv f) (g : G₁ →* G₃) (hg : f.ker g.ker) (h : G₂ →* G₃) (hh : h.comp f = g) :
h = (f.lift_of_right_inverse f_inv hf) g, hg⟩
theorem subgroup.normal.comap {G : Type u_1} [group G] {N : Type u_4} [group N] {H : subgroup N} (hH : H.normal) (f : G →* N) :
theorem add_subgroup.normal.comap {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {H : add_subgroup N} (hH : H.normal) (f : G →+ N) :
@[protected, instance]
def subgroup.normal_comap {G : Type u_1} [group G] {N : Type u_4} [group N] {H : subgroup N} [nH : H.normal] (f : G →* N) :
@[protected, instance]
def add_subgroup.normal_comap {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {H : add_subgroup N} [nH : H.normal] (f : G →+ N) :
theorem subgroup.normal.subgroup_of {G : Type u_1} [group G] {H : subgroup G} (hH : H.normal) (K : subgroup G) :
@[protected, instance]
@[protected, instance]
def subgroup.normal_subgroup_of {G : Type u_1} [group G] {H N : subgroup G} [N.normal] :
@[simp]
def monoid_hom.subgroup_comap {G : Type u_1} {G' : Type u_2} [group G] [group G'] (f : G →* G') (H' : subgroup G') :

The monoid_hom from the preimage of a subgroup to itself.

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

the add_monoid_hom from the preimage of an additive subgroup to itself.

Equations
@[simp]
theorem monoid_hom.subgroup_comap_apply_coe {G : Type u_1} {G' : Type u_2} [group G] [group G'] (f : G →* G') (H' : subgroup G') (x : (submonoid.comap f H'.to_submonoid)) :
def monoid_hom.subgroup_map {G : Type u_1} {G' : Type u_2} [group G] [group G'] (f : G →* G') (H : subgroup G) :

The monoid_hom from a subgroup to its image.

Equations
@[simp]
theorem monoid_hom.subgroup_map_apply_coe {G : Type u_1} {G' : Type u_2} [group G] [group G'] (f : G →* G') (H : subgroup G) (x : (H.to_submonoid)) :
@[simp]
theorem add_monoid_hom.add_subgroup_map_apply_coe {G : Type u_1} {G' : Type u_2} [add_group G] [add_group G'] (f : G →+ G') (H : add_subgroup G) (x : (H.to_add_submonoid)) :
def add_monoid_hom.add_subgroup_map {G : Type u_1} {G' : Type u_2} [add_group G] [add_group G'] (f : G →+ G') (H : add_subgroup G) :

the add_monoid_hom from an additive subgroup to its image

Equations
theorem monoid_hom.subgroup_map_surjective {G : Type u_1} {G' : Type u_2} [group G] [group G'] (f : G →* G') (H : subgroup G) :
def mul_equiv.subgroup_congr {G : Type u_1} [group G] {H K : subgroup G} (h : H = K) :

Makes the identity isomorphism from a proof two subgroups of a multiplicative group are equal.

Equations
def add_equiv.add_subgroup_congr {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H = K) :

Makes the identity additive isomorphism from a proof two subgroups of an additive group are equal.

Equations
def mul_equiv.subgroup_map {G : Type u_1} {G' : Type u_2} [group G] [group G'] (e : G ≃* G') (H : subgroup G) :

A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use subgroup.equiv_map_of_injective.

Equations
def add_equiv.add_subgroup_map {G : Type u_1} {G' : Type u_2} [add_group G] [add_group G'] (e : G ≃+ G') (H : add_subgroup G) :

An additive subgroup is isomorphic to its image under an an isomorphism. If you only have an injective map, use add_subgroup.equiv_map_of_injective.

Equations
@[simp]
theorem add_equiv.coe_add_subgroup_map_apply {G : Type u_1} {G' : Type u_2} [add_group G] [add_group G'] (e : G ≃+ G') (H : add_subgroup G) (g : H) :
@[simp]
theorem mul_equiv.coe_subgroup_map_apply {G : Type u_1} {G' : Type u_2} [group G] [group G'] (e : G ≃* G') (H : subgroup G) (g : H) :
@[simp]
theorem add_equiv.add_subgroup_map_symm_apply {G : Type u_1} {G' : Type u_2} [add_group G] [add_group G'] (e : G ≃+ G') (H : add_subgroup G) (g : (add_subgroup.map e H)) :
((e.add_subgroup_map H).symm) g = (e.symm) g, _⟩
@[simp]
theorem mul_equiv.subgroup_map_symm_apply {G : Type u_1} {G' : Type u_2} [group G] [group G'] (e : G ≃* G') (H : subgroup G) (g : (subgroup.map e H)) :
((e.subgroup_map H).symm) g = (e.symm) g, _⟩
@[simp]
theorem subgroup.equiv_map_of_injective_coe_mul_equiv {G : Type u_1} {G' : Type u_2} [group G] [group G'] (H : subgroup G) (e : G ≃* G') :
theorem add_subgroup.mem_sup {C : Type u_5} [add_comm_group C] {s t : add_subgroup C} {x : C} :
x s t (y : C) (H : y s) (z : C) (H : z t), y + z = x
theorem subgroup.mem_sup {C : Type u_5} [comm_group C] {s t : subgroup C} {x : C} :
x s t (y : C) (H : y s) (z : C) (H : z t), y * z = x
theorem add_subgroup.mem_sup' {C : Type u_5} [add_comm_group C] {s t : add_subgroup C} {x : C} :
x s t (y : s) (z : t), y + z = x
theorem subgroup.mem_sup' {C : Type u_5} [comm_group C] {s t : subgroup C} {x : C} :
x s t (y : s) (z : t), y * z = x
theorem add_subgroup.mem_closure_pair {C : Type u_5} [add_comm_group C] {x y z : C} :
z add_subgroup.closure {x, y} (m n : ), m x + n y = z
theorem subgroup.mem_closure_pair {C : Type u_5} [comm_group C] {x y z : C} :
z subgroup.closure {x, y} (m n : ), x ^ m * y ^ n = z
@[protected, instance]
theorem subgroup.normal_subgroup_of_iff {G : Type u_1} [group G] {H K : subgroup G} (hHK : H K) :
(H.subgroup_of K).normal (h k : G), h H k K k * h * k⁻¹ H
theorem add_subgroup.normal_add_subgroup_of_iff {G : Type u_1} [add_group G] {H K : add_subgroup G} (hHK : H K) :
(H.add_subgroup_of K).normal (h k : G), h H k K k + h + -k H
@[protected, instance]
def add_subgroup.sum_add_subgroup_of_sum_normal {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] {H₁ K₁ : add_subgroup G} {H₂ K₂ : add_subgroup N} [h₁ : (H₁.add_subgroup_of K₁).normal] [h₂ : (H₂.add_subgroup_of K₂).normal] :
((H₁.prod H₂).add_subgroup_of (K₁.prod K₂)).normal
@[protected, instance]
def subgroup.prod_subgroup_of_prod_normal {G : Type u_1} [group G] {N : Type u_4} [group N] {H₁ K₁ : subgroup G} {H₂ K₂ : subgroup N} [h₁ : (H₁.subgroup_of K₁).normal] [h₂ : (H₂.subgroup_of K₂).normal] :
((H₁.prod H₂).subgroup_of (K₁.prod K₂)).normal
@[protected, instance]
def add_subgroup.sum_normal {G : Type u_1} [add_group G] {N : Type u_4} [add_group N] (H : add_subgroup G) (K : add_subgroup N) [hH : H.normal] [hK : K.normal] :
(H.prod K).normal
@[protected, instance]
def subgroup.prod_normal {G : Type u_1} [group G] {N : Type u_4} [group N] (H : subgroup G) (K : subgroup N) [hH : H.normal] [hK : K.normal] :
(H.prod K).normal
theorem subgroup.inf_subgroup_of_inf_normal_of_right {G : Type u_1} [group G] (A B' B : subgroup G) (hB : B' B) [hN : (B'.subgroup_of B).normal] :
((A B').subgroup_of (A B)).normal
theorem add_subgroup.inf_add_subgroup_of_inf_normal_of_right {G : Type u_1} [add_group G] (A B' B : add_subgroup G) (hB : B' B) [hN : (B'.add_subgroup_of B).normal] :
((A B').add_subgroup_of (A B)).normal
theorem subgroup.inf_subgroup_of_inf_normal_of_left {G : Type u_1} [group G] {A' A : subgroup G} (B : subgroup G) (hA : A' A) [hN : (A'.subgroup_of A).normal] :
((A' B).subgroup_of (A B)).normal
theorem add_subgroup.inf_add_subgroup_of_inf_normal_of_left {G : Type u_1} [add_group G] {A' A : add_subgroup G} (B : add_subgroup G) (hA : A' A) [hN : (A'.add_subgroup_of A).normal] :
((A' B).add_subgroup_of (A B)).normal
@[protected, instance]
def subgroup.normal_inf_normal {G : Type u_1} [group G] (H K : subgroup G) [hH : H.normal] [hK : K.normal] :
(H K).normal
@[protected, instance]
def add_subgroup.normal_inf_normal {G : Type u_1} [add_group G] (H K : add_subgroup G) [hH : H.normal] [hK : K.normal] :
(H K).normal
theorem add_subgroup.add_subgroup_of_sup {G : Type u_1} [add_group G] (A A' B : add_subgroup G) (hA : A B) (hA' : A' B) :
theorem subgroup.subgroup_of_sup {G : Type u_1} [group G] (A A' B : subgroup G) (hA : A B) (hA' : A' B) :
theorem add_subgroup.subgroup_normal.mem_comm {G : Type u_1} [add_group G] {H K : add_subgroup G} (hK : H K) [hN : (H.add_subgroup_of K).normal] {a b : G} (hb : b K) (h : a + b H) :
b + a H
theorem subgroup.subgroup_normal.mem_comm {G : Type u_1} [group G] {H K : subgroup G} (hK : H K) [hN : (H.subgroup_of K).normal] {a b : G} (hb : b K) (h : a * b H) :
b * a H
theorem subgroup.commute_of_normal_of_disjoint {G : Type u_1} [group G] (H₁ H₂ : subgroup G) (hH₁ : H₁.normal) (hH₂ : H₂.normal) (hdis : disjoint H₁ H₂) (x y : G) (hx : x H₁) (hy : y H₂) :

Elements of disjoint, normal subgroups commute.

theorem add_subgroup.commute_of_normal_of_disjoint {G : Type u_1} [add_group G] (H₁ H₂ : add_subgroup G) (hH₁ : H₁.normal) (hH₂ : H₂.normal) (hdis : disjoint H₁ H₂) (x y : G) (hx : x H₁) (hy : y H₂) :

Elements of disjoint, normal subgroups commute.

theorem add_subgroup.disjoint_def {G : Type u_1} [add_group G] {H₁ H₂ : add_subgroup G} :
disjoint H₁ H₂ {x : G}, x H₁ x H₂ x = 0
theorem subgroup.disjoint_def {G : Type u_1} [group G] {H₁ H₂ : subgroup G} :
disjoint H₁ H₂ {x : G}, x H₁ x H₂ x = 1
theorem subgroup.disjoint_def' {G : Type u_1} [group G] {H₁ H₂ : subgroup G} :
disjoint H₁ H₂ {x y : G}, x H₁ y H₂ x = y x = 1
theorem add_subgroup.disjoint_def' {G : Type u_1} [add_group G] {H₁ H₂ : add_subgroup G} :
disjoint H₁ H₂ {x y : G}, x H₁ y H₂ x = y x = 0
theorem add_subgroup.disjoint_iff_add_eq_zero {G : Type u_1} [add_group G] {H₁ H₂ : add_subgroup G} :
disjoint H₁ H₂ {x y : G}, x H₁ y H₂ x + y = 0 x = 0 y = 0
theorem subgroup.disjoint_iff_mul_eq_one {G : Type u_1} [group G] {H₁ H₂ : subgroup G} :
disjoint H₁ H₂ {x y : G}, x H₁ y H₂ x * y = 1 x = 1 y = 1
theorem subgroup.mul_injective_of_disjoint {G : Type u_1} [group G] {H₁ H₂ : subgroup G} (h : disjoint H₁ H₂) :
function.injective (λ (g : H₁ × H₂), (g.fst) * (g.snd))
theorem add_subgroup.add_injective_of_disjoint {G : Type u_1} [add_group G] {H₁ H₂ : add_subgroup G} (h : disjoint H₁ H₂) :
function.injective (λ (g : H₁ × H₂), (g.fst) + (g.snd))
theorem is_conj.normal_closure_eq_top_of {G : Type u_1} [group G] {N : subgroup G} [hn : N.normal] {g g' : G} {hg : g N} {hg' : g' N} (hc : is_conj g g') (ht : subgroup.normal_closure {g, hg⟩} = ) :
theorem is_conj.eq_of_left_mem_center {M : Type u_5} [monoid M] {g h : M} (H : is_conj g h) (Hg : g set.center M) :
g = h
theorem is_conj.eq_of_right_mem_center {M : Type u_5} [monoid M] {g h : M} (H : is_conj g h) (Hh : h set.center M) :
g = h