mathlib documentation

group_theory.subgroup.basic

Subgroups #

This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled form (unbundled subgroups are in deprecated/subgroups.lean).

We prove subgroups of a group form a complete lattice, and results about images and preimages of subgroups under group homomorphisms. The bundled subgroups use bundled monoid homomorphisms.

There are also theorems about the subgroups generated by an element or a subset of a group, defined both inductively and as the infimum of the set of subgroups containing a given element/subset.

Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.

Main definitions #

Notation used here:

Definitions in the file:

Implementation notes #

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

Tags #

subgroup, subgroups

source
def subgroup.to_submonoid {G : Type u_3} [group G] (self : subgroup G) :
submonoid G

Reinterpret a subgroup as a submonoid.

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

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

source
structure add_subgroup (G : Type u_3) [add_group G] :
Type u_3

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

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

Reinterpret an add_subgroup as an add_submonoid.

source
@[instance]
def subgroup.set_like {G : Type u_1} [group G] :
set_like (subgroup G) G
Equations
source
@[instance]
def add_subgroup.set_like {G : Type u_1} [add_group G] :
set_like (add_subgroup G) G
Equations
source
@[simp]
theorem subgroup.mem_carrier {G : Type u_1} [group G] {s : subgroup G} {x : G} :
x ∈ s.carrier ↔ x ∈ s
source
@[simp]
theorem add_subgroup.mem_carrier {G : Type u_1} [add_group G] {s : add_subgroup G} {x : G} :
x ∈ s.carrier ↔ x ∈ s
source
@[simp]
theorem add_subgroup.mem_mk {G : Type u_1} [add_group G] {s : set G} {x : G} (h_one : 0 ∈ s) (h_mul : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) (h_inv : ∀ {x : G}, x ∈ s → -x ∈ s) :
x ∈ {carrier := s, zero_mem' := h_one, add_mem' := h_mul, neg_mem' := h_inv} ↔ x ∈ s
source
@[simp]
theorem subgroup.mem_mk {G : Type u_1} [group G] {s : set G} {x : G} (h_one : 1 ∈ s) (h_mul : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s) (h_inv : ∀ {x : G}, x ∈ s → x⁻¹ ∈ s) :
x ∈ {carrier := s, one_mem' := h_one, mul_mem' := h_mul, inv_mem' := h_inv} ↔ x ∈ s
source
@[simp]
theorem subgroup.coe_set_mk {G : Type u_1} [group G] {s : set G} (h_one : 1 ∈ s) (h_mul : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s) (h_inv : ∀ {x : G}, x ∈ s → x⁻¹ ∈ s) :
↑{carrier := s, one_mem' := h_one, mul_mem' := h_mul, inv_mem' := h_inv} = s
source
@[simp]
theorem add_subgroup.coe_set_mk {G : Type u_1} [add_group G] {s : set G} (h_one : 0 ∈ s) (h_mul : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) (h_inv : ∀ {x : G}, x ∈ s → -x ∈ s) :
↑{carrier := s, zero_mem' := h_one, add_mem' := h_mul, neg_mem' := h_inv} = s
source
@[simp]
theorem add_subgroup.mk_le_mk {G : Type u_1} [add_group G] {s t : set G} (h_one : 0 ∈ s) (h_mul : ∀ {a b : G}, a ∈ s → b ∈ s → a + b ∈ s) (h_inv : ∀ {x : G}, x ∈ s → -x ∈ s) (h_one' : 0 ∈ t) (h_mul' : ∀ {a b : G}, a ∈ t → b ∈ t → a + b ∈ t) (h_inv' : ∀ {x : G}, x ∈ t → -x ∈ t) :
{carrier := s, zero_mem' := h_one, add_mem' := h_mul, neg_mem' := h_inv} ≤ {carrier := t, zero_mem' := h_one', add_mem' := h_mul', neg_mem' := h_inv'} ↔ s ⊆ t
source
@[simp]
theorem subgroup.mk_le_mk {G : Type u_1} [group G] {s t : set G} (h_one : 1 ∈ s) (h_mul : ∀ {a b : G}, a ∈ s → b ∈ s → a * b ∈ s) (h_inv : ∀ {x : G}, x ∈ s → x⁻¹ ∈ s) (h_one' : 1 ∈ t) (h_mul' : ∀ {a b : G}, a ∈ t → b ∈ t → a * b ∈ t) (h_inv' : ∀ {x : G}, x ∈ t → x⁻¹ ∈ t) :
{carrier := s, one_mem' := h_one, mul_mem' := h_mul, inv_mem' := h_inv} ≤ {carrier := t, one_mem' := h_one', mul_mem' := h_mul', inv_mem' := h_inv'} ↔ s ⊆ t
source
def subgroup.simps.coe {G : Type u_1} [group G] (S : subgroup G) :
set G

See Note [custom simps projection]

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

See Note [custom simps projection]

Equations
source
@[simp]
theorem add_subgroup.coe_to_add_submonoid {G : Type u_1} [add_group G] (K : add_subgroup G) :
↑(K.to_add_submonoid) = ↑K
source
@[simp]
theorem subgroup.coe_to_submonoid {G : Type u_1} [group G] (K : subgroup G) :
↑(K.to_submonoid) = ↑K
source
@[simp]
theorem subgroup.mem_to_submonoid {G : Type u_1} [group G] (K : subgroup G) (x : G) :
x ∈ K.to_submonoid ↔ x ∈ K
source
@[simp]
theorem add_subgroup.mem_to_add_submonoid {G : Type u_1} [add_group G] (K : add_subgroup G) (x : G) :
x ∈ K.to_add_submonoid ↔ x ∈ K
source
@[instance]
def subgroup.fintype {G : Type u_1} [group G] (K : subgroup G) [d : decidable_pred (λ (_x : G), _x ∈ K)] [fintype G] :
fintype ↥K
Equations
source
@[instance]
def add_subgroup.fintype {G : Type u_1} [add_group G] (K : add_subgroup G) [d : decidable_pred (λ (_x : G), _x ∈ K)] [fintype G] :
fintype ↥K
Equations
source
theorem add_subgroup.to_add_submonoid_injective {G : Type u_1} [add_group G] :
function.injective add_subgroup.to_add_submonoid
source
theorem subgroup.to_submonoid_injective {G : Type u_1} [group G] :
function.injective subgroup.to_submonoid
source
@[simp]
theorem add_subgroup.to_add_submonoid_eq {G : Type u_1} [add_group G] {p q : add_subgroup G} :
p.to_add_submonoid = q.to_add_submonoid ↔ p = q
source
@[simp]
theorem subgroup.to_submonoid_eq {G : Type u_1} [group G] {p q : subgroup G} :
p.to_submonoid = q.to_submonoid ↔ p = q
source
theorem subgroup.to_submonoid_strict_mono {G : Type u_1} [group G] :
strict_mono subgroup.to_submonoid
source
theorem add_subgroup.to_add_submonoid_strict_mono {G : Type u_1} [add_group G] :
strict_mono add_subgroup.to_add_submonoid
source
theorem subgroup.to_submonoid_mono {G : Type u_1} [group G] :
monotone subgroup.to_submonoid
source
theorem add_subgroup.to_add_submonoid_mono {G : Type u_1} [add_group G] :
monotone add_subgroup.to_add_submonoid
source
@[simp]
theorem add_subgroup.to_add_submonoid_le {G : Type u_1} [add_group G] {p q : add_subgroup G} :
p.to_add_submonoid ≤ q.to_add_submonoid ↔ p ≤ q
source
@[simp]
theorem subgroup.to_submonoid_le {G : Type u_1} [group G] {p q : subgroup G} :
p.to_submonoid ≤ q.to_submonoid ↔ p ≤ q

Conversion to/from additive/multiplicative #

source
def subgroup.to_add_subgroup {G : Type u_1} [group G] :
subgroup G ≃o add_subgroup (additive G)

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

Equations
source
@[simp]
theorem subgroup.to_add_subgroup_apply_coe {G : Type u_1} [group G] (S : subgroup G) :
↑(⇑subgroup.to_add_subgroup S) = (⇑submonoid.to_add_submonoid S.to_submonoid).carrier
source
@[simp]
theorem subgroup.to_add_subgroup_symm_apply_coe {G : Type u_1} [group G] (S : add_subgroup (additive G)) :
↑(⇑(rel_iso.symm subgroup.to_add_subgroup) S) = (⇑add_submonoid.to_submonoid' S.to_add_submonoid).carrier
source
def add_subgroup.to_subgroup' {G : Type u_1} [group G] :
add_subgroup (additive G) ≃o subgroup G

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

source
def add_subgroup.to_subgroup {A : Type u_2} [add_group A] :
add_subgroup A ≃o subgroup (multiplicative A)

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

Equations
source
@[simp]
theorem add_subgroup.to_subgroup_apply_coe {A : Type u_2} [add_group A] (S : add_subgroup A) :
↑(⇑add_subgroup.to_subgroup S) = (⇑add_submonoid.to_submonoid S.to_add_submonoid).carrier
source
@[simp]
theorem add_subgroup.to_subgroup_symm_apply_coe {A : Type u_2} [add_group A] (S : subgroup (multiplicative A)) :
↑(⇑(rel_iso.symm add_subgroup.to_subgroup) S) = (⇑submonoid.to_add_submonoid' S.to_submonoid).carrier
source
def subgroup.to_add_subgroup' {A : Type u_2} [add_group A] :
subgroup (multiplicative A) ≃o add_subgroup A

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

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

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

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

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

Equations
source
@[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
source
theorem subgroup.copy_eq {G : Type u_1} [group G] (K : subgroup G) (s : set G) (hs : s = ↑K) :
K.copy s hs = K
source
@[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.

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

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

A subgroup contains the group's 1.

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

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

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

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

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

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

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

source
@[simp]
theorem add_subgroup.neg_mem_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {x : G} :
-x ∈ H ↔ x ∈ H
source
@[simp]
theorem subgroup.inv_mem_iff {G : Type u_1} [group G] (H : subgroup G) {x : G} :
x⁻¹ ∈ H ↔ x ∈ H
source
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
source
theorem subgroup.div_mem_comm_iff {G : Type u_1} [group G] (H : subgroup G) {a b : G} :
a / b ∈ H ↔ b / a ∈ H
source
@[simp]
theorem add_subgroup.neg_coe_set {G : Type u_1} [add_group G] (H : add_subgroup G) :
-↑H = ↑H
source
@[simp]
theorem subgroup.inv_coe_set {G : Type u_1} [group G] (H : subgroup G) :
(↑H)⁻¹ = ↑H
source
@[simp]
theorem subgroup.exists_inv_mem_iff_exists_mem {G : Type u_1} [group G] (K : subgroup G) {P : G → Prop} :
(∃ (x : G), x ∈ K ∧ P x⁻¹) ↔ ∃ (x : G) (H : x ∈ K), P x
source
@[simp]
theorem add_subgroup.exists_neg_mem_iff_exists_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {P : G → Prop} :
(∃ (x : G), x ∈ K ∧ P (-x)) ↔ ∃ (x : G) (H : x ∈ K), P x
source
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
source
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
source
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
source
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
source
theorem subgroup.list_prod_mem {G : Type u_1} [group G] (K : subgroup G) {l : list G} :
(∀ (x : G), x ∈ l → x ∈ K) → l.prod ∈ K

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

source
theorem add_subgroup.list_sum_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {l : list G} :
(∀ (x : G), x ∈ l → x ∈ K) → l.sum ∈ K

Sum of a list of elements in an add_subgroup is in the add_subgroup.

source
theorem add_subgroup.multiset_sum_mem {G : Type u_1} [add_comm_group G] (K : add_subgroup G) (g : multiset G) :
(∀ (a : G), a ∈ g → a ∈ K) → g.sum ∈ K

Sum of a multiset of elements in an add_subgroup of an add_comm_group is in the add_subgroup.

source
theorem subgroup.multiset_prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) (g : multiset G) :
(∀ (a : G), a ∈ g → a ∈ K) → g.prod ∈ K

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

source
theorem add_subgroup.sum_mem {G : Type u_1} [add_comm_group G] (K : add_subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (h : ∀ (c : ι), c ∈ t → f c ∈ K) :
∑ (c : ι) in t, f c ∈ K

Sum of elements in an add_subgroup of an add_comm_group indexed by a finset is in the add_subgroup.

source
theorem subgroup.prod_mem {G : Type u_1} [comm_group G] (K : subgroup G) {ι : Type u_2} {t : finset ι} {f : ι → G} (h : ∀ (c : ι), c ∈ t → f c ∈ K) :
∏ (c : ι) in t, f c ∈ K

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

source
theorem subgroup.pow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x ∈ K) (n : ℕ) :
x ^ n ∈ K
source
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
source
theorem add_subgroup.gsmul_mem {G : Type u_1} [add_group G] (K : add_subgroup G) {x : G} (hx : x ∈ K) (n : ℤ) :
n • x ∈ K
source
theorem subgroup.gpow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x ∈ K) (n : ℤ) :
x ^ n ∈ K
source
def subgroup.of_div {G : Type u_1} [group G] (s : set G) (hsn : s.nonempty) (hs : ∀ (x y : G), x ∈ s → y ∈ s → x * y⁻¹ ∈ s) :
subgroup G

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

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

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

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

A subgroup of a group inherits a multiplication.

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

An add_subgroup of an add_group inherits an addition.

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

A subgroup of a group inherits a 1.

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

An add_subgroup of an add_group inherits a zero.

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

A add_subgroup of a add_group inherits an inverse.

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

A subgroup of a group inherits an inverse.

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

A subgroup of a group inherits a division

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

An add_subgroup of an add_group inherits a subtraction.

Equations
source
@[simp]
theorem add_subgroup.coe_add {G : Type u_1} [add_group G] (H : add_subgroup G) (x y : ↥H) :
↑(x + y) = ↑x + ↑y
source
@[simp]
theorem subgroup.coe_mul {G : Type u_1} [group G] (H : subgroup G) (x y : ↥H) :
↑x * y = (↑x) * ↑y
source
@[simp]
theorem add_subgroup.coe_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :
↑0 = 0
source
@[simp]
theorem subgroup.coe_one {G : Type u_1} [group G] (H : subgroup G) :
↑1 = 1
source
@[simp]
theorem add_subgroup.coe_neg {G : Type u_1} [add_group G] (H : add_subgroup G) (x : ↥H) :
↑-x = -↑x
source
@[simp]
theorem subgroup.coe_inv {G : Type u_1} [group G] (H : subgroup G) (x : ↥H) :
↑x⁻¹ = (↑x)⁻¹
source
@[simp]
theorem subgroup.coe_div {G : Type u_1} [group G] (H : subgroup G) (x y : ↥H) :
↑(x / y) = ↑x / ↑y
source
@[simp]
theorem add_subgroup.coe_sub {G : Type u_1} [add_group G] (H : add_subgroup G) (x y : ↥H) :
↑(x - y) = ↑x - ↑y
source
@[simp]
theorem add_subgroup.coe_mk {G : Type u_1} [add_group G] (H : add_subgroup G) (x : G) (hx : x ∈ H) :
↑⟨x, hx⟩ = x
source
@[simp]
theorem subgroup.coe_mk {G : Type u_1} [group G] (H : subgroup G) (x : G) (hx : x ∈ H) :
↑⟨x, hx⟩ = x
source
@[instance]
def subgroup.to_group {G : Type u_1} [group G] (H : subgroup G) :
group ↥H

A subgroup of a group inherits a group structure.

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

An add_subgroup of an add_group inherits an add_group structure.

Equations
source
@[instance]
def add_subgroup.to_add_comm_group {G : Type u_1} [add_comm_group G] (H : add_subgroup G) :
add_comm_group ↥H

An add_subgroup of an add_comm_group is an add_comm_group.

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

A subgroup of a comm_group is a comm_group.

Equations
source
@[instance]
def add_subgroup.to_ordered_add_comm_group {G : Type u_1} [ordered_add_comm_group G] (H : add_subgroup G) :
ordered_add_comm_group ↥H

An add_subgroup of an add_ordered_comm_group is an add_ordered_comm_group.

Equations
source
@[instance]
def subgroup.to_ordered_comm_group {G : Type u_1} [ordered_comm_group G] (H : subgroup G) :
ordered_comm_group ↥H

A subgroup of an ordered_comm_group is an ordered_comm_group.

Equations
source
@[instance]
def subgroup.to_linear_ordered_comm_group {G : Type u_1} [linear_ordered_comm_group G] (H : subgroup G) :
linear_ordered_comm_group ↥H

A subgroup of a linear_ordered_comm_group is a linear_ordered_comm_group.

Equations
source
@[instance]
def add_subgroup.to_linear_ordered_add_comm_group {G : Type u_1} [linear_ordered_add_comm_group G] (H : add_subgroup G) :
linear_ordered_add_comm_group ↥H

An add_subgroup of a linear_ordered_add_comm_group is a linear_ordered_add_comm_group.

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

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

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

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

Equations
source
@[simp]
theorem subgroup.coe_subtype {G : Type u_1} [group G] (H : subgroup G) :
⇑(H.subtype) = coe
source
@[simp]
theorem add_subgroup.coe_subtype {G : Type u_1} [add_group G] (H : add_subgroup G) :
⇑(H.subtype) = coe
source
@[simp]
theorem subgroup.coe_pow {G : Type u_1} [group G] (H : subgroup G) (x : ↥H) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
@[simp]
theorem subgroup.coe_gpow {G : Type u_1} [group G] (H : subgroup G) (x : ↥H) (n : ℤ) :
↑(x ^ n) = ↑x ^ n
source
def add_subgroup.inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) :
↥H →+ ↥K

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

Equations
source
def subgroup.inclusion {G : Type u_1} [group G] {H K : subgroup G} (h : H ≤ K) :
↥H →* ↥K

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

Equations
source
@[simp]
theorem subgroup.coe_inclusion {G : Type u_1} [group G] {H K : subgroup G} {h : H ≤ K} (a : ↥H) :
↑(⇑(subgroup.inclusion h) a) = ↑a
source
@[simp]
theorem add_subgroup.coe_inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} {h : H ≤ K} (a : ↥H) :
↑(⇑(add_subgroup.inclusion h) a) = ↑a
source
@[simp]
theorem add_subgroup.subtype_comp_inclusion {G : Type u_1} [add_group G] {H K : add_subgroup G} (hH : H ≤ K) :
K.subtype.comp (add_subgroup.inclusion hH) = H.subtype
source
@[simp]
theorem subgroup.subtype_comp_inclusion {G : Type u_1} [group G] {H K : subgroup G} (hH : H ≤ K) :
K.subtype.comp (subgroup.inclusion hH) = H.subtype
source
@[instance]
def add_subgroup.has_top {G : Type u_1} [add_group G] :
has_top (add_subgroup G)

The add_subgroup G of the add_group G.

Equations
source
@[instance]
def subgroup.has_top {G : Type u_1} [group G] :
has_top (subgroup G)

The subgroup G of the group G.

Equations
source
@[instance]
def add_subgroup.has_bot {G : Type u_1} [add_group G] :
has_bot (add_subgroup G)

The trivial add_subgroup {0} of an add_group G.

Equations
source
@[instance]
def subgroup.has_bot {G : Type u_1} [group G] :
has_bot (subgroup G)

The trivial subgroup {1} of an group G.

Equations
source
@[instance]
def add_subgroup.inhabited {G : Type u_1} [add_group G] :
inhabited (add_subgroup G)
Equations
source
@[instance]
def subgroup.inhabited {G : Type u_1} [group G] :
inhabited (subgroup G)
Equations
source
@[simp]
theorem subgroup.mem_bot {G : Type u_1} [group G] {x : G} :
x ∈ ⊥ ↔ x = 1
source
@[simp]
theorem add_subgroup.mem_bot {G : Type u_1} [add_group G] {x : G} :
x ∈ ⊥ ↔ x = 0
source
@[simp]
theorem add_subgroup.mem_top {G : Type u_1} [add_group G] (x : G) :
x ∈ ⊤
source
@[simp]
theorem subgroup.mem_top {G : Type u_1} [group G] (x : G) :
x ∈ ⊤
source
@[simp]
theorem subgroup.coe_top {G : Type u_1} [group G] :
↑⊤ = set.univ
source
@[simp]
theorem add_subgroup.coe_top {G : Type u_1} [add_group G] :
↑⊤ = set.univ
source
@[simp]
theorem add_subgroup.coe_bot {G : Type u_1} [add_group G] :
↑⊥ = {0}
source
@[simp]
theorem subgroup.coe_bot {G : Type u_1} [group G] :
↑⊥ = {1}
source
@[instance]
def add_subgroup.has_bot.bot.unique {G : Type u_1} [add_group G] :
unique ↥⊥
Equations
source
@[instance]
def subgroup.has_bot.bot.unique {G : Type u_1} [group G] :
unique ↥⊥
Equations
source
theorem subgroup.eq_bot_iff_forall {G : Type u_1} [group G] (H : subgroup G) :
H = ⊥ ↔ ∀ (x : G), x ∈ H → x = 1
source
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
source
theorem subgroup.eq_bot_of_subsingleton {G : Type u_1} [group G] (H : subgroup G) [subsingleton ↥H] :
H = ⊥
source
theorem add_subgroup.eq_bot_of_subsingleton {G : Type u_1} [add_group G] (H : add_subgroup G) [subsingleton ↥H] :
H = ⊥
source
@[instance]
def subgroup.fintype_bot {G : Type u_1} [group G] :
fintype ↥⊥
Equations
source
@[instance]
def add_subgroup.fintype_bot {G : Type u_1} [add_group G] :
fintype ↥⊥
Equations
source
@[simp]
theorem subgroup.card_bot {G : Type u_1} [group G] {_x : fintype ↥⊥} :
fintype.card ↥⊥ = 1
source
@[simp]
theorem add_subgroup.card_bot {G : Type u_1} [add_group G] {_x : fintype ↥⊥} :
fintype.card ↥⊥ = 1
source
theorem subgroup.eq_top_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] [fintype G] (h : fintype.card ↥H = fintype.card G) :
H = ⊤
source
theorem add_subgroup.eq_top_of_card_eq {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] [fintype G] (h : fintype.card ↥H = fintype.card G) :
H = ⊤
source
theorem subgroup.eq_top_of_le_card {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] [fintype G] (h : fintype.card G ≤ fintype.card ↥H) :
H = ⊤
source
theorem add_subgroup.eq_top_of_le_card {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] [fintype G] (h : fintype.card G ≤ fintype.card ↥H) :
H = ⊤
source
theorem subgroup.eq_bot_of_card_le {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] (h : fintype.card ↥H ≤ 1) :
H = ⊥
source
theorem add_subgroup.eq_bot_of_card_le {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] (h : fintype.card ↥H ≤ 1) :
H = ⊥
source
theorem add_subgroup.eq_bot_of_card_eq {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] (h : fintype.card ↥H = 1) :
H = ⊥
source
theorem subgroup.eq_bot_of_card_eq {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] (h : fintype.card ↥H = 1) :
H = ⊥
source
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
source
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
source
theorem subgroup.bot_or_nontrivial {G : Type u_1} [group G] (H : subgroup G) :
H = ⊥ ∨ nontrivial ↥H

A subgroup is either the trivial subgroup or nontrivial.

source
theorem add_subgroup.bot_or_nontrivial {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = ⊥ ∨ nontrivial ↥H
source
theorem subgroup.bot_or_exists_ne_one {G : Type u_1} [group G] (H : subgroup G) :
H = ⊥ ∨ ∃ (x : G) (H : x ∈ H), x ≠ 1

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

source
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
source
theorem add_subgroup.card_nonpos_iff_eq_bot {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype ↥H] :
fintype.card ↥H ≤ 1 ↔ H = ⊥
source
theorem subgroup.card_le_one_iff_eq_bot {G : Type u_1} [group G] (H : subgroup G) [fintype ↥H] :
fintype.card ↥H ≤ 1 ↔ H = ⊥
source
@[instance]
def subgroup.has_inf {G : Type u_1} [group G] :
has_inf (subgroup G)

The inf of two subgroups is their intersection.

Equations
source
@[instance]
def add_subgroup.has_inf {G : Type u_1} [add_group G] :
has_inf (add_subgroup G)

The inf of two add_subgroupss is their intersection.

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

Subgroups of a group form a complete lattice.

Equations
source
@[instance]
def add_subgroup.complete_lattice {G : Type u_1} [add_group G] :
complete_lattice (add_subgroup G)

The add_subgroups of an add_group form a complete lattice.

Equations
source
theorem subgroup.mem_sup_left {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x ∈ S → x ∈ S ⊔ T
source
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
source
theorem subgroup.mem_sup_right {G : Type u_1} [group G] {S T : subgroup G} {x : G} :
x ∈ T → x ∈ S ⊔ T
source
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
source
theorem subgroup.mem_supr_of_mem {G : Type u_1} [group G] {ι : Type u_2} {S : ι → subgroup G} (i : ι) {x : G} :
x ∈ S i → x ∈ supr S
source
theorem add_subgroup.mem_supr_of_mem {G : Type u_1} [add_group G] {ι : Type u_2} {S : ι → add_subgroup G} (i : ι) {x : G} :
x ∈ S i → x ∈ supr S
source
theorem subgroup.mem_Sup_of_mem {G : Type u_1} [group G] {S : set (subgroup G)} {s : subgroup G} (hs : s ∈ S) {x : G} :
x ∈ s → x ∈ Sup S
source
theorem add_subgroup.mem_Sup_of_mem {G : Type u_1} [add_group G] {S : set (add_subgroup G)} {s : add_subgroup G} (hs : s ∈ S) {x : G} :
x ∈ s → x ∈ Sup S
source
@[simp]
theorem subgroup.subsingleton_iff {G : Type u_1} [group G] :
subsingleton (subgroup G) ↔ subsingleton G
source
@[simp]
theorem add_subgroup.subsingleton_iff {G : Type u_1} [add_group G] :
subsingleton (add_subgroup G) ↔ subsingleton G
source
@[simp]
theorem subgroup.nontrivial_iff {G : Type u_1} [group G] :
nontrivial (subgroup G) ↔ nontrivial G
source
@[simp]
theorem add_subgroup.nontrivial_iff {G : Type u_1} [add_group G] :
nontrivial (add_subgroup G) ↔ nontrivial G
source
@[instance]
def add_subgroup.unique {G : Type u_1} [add_group G] [subsingleton G] :
unique (add_subgroup G)
Equations
source
@[instance]
def subgroup.unique {G : Type u_1} [group G] [subsingleton G] :
unique (subgroup G)
Equations
source
@[instance]
def subgroup.nontrivial {G : Type u_1} [group G] [nontrivial G] :
nontrivial (subgroup G)
source
@[instance]
def add_subgroup.nontrivial {G : Type u_1} [add_group G] [nontrivial G] :
nontrivial (add_subgroup G)
source
theorem add_subgroup.eq_top_iff' {G : Type u_1} [add_group G] (H : add_subgroup G) :
H = ⊤ ↔ ∀ (x : G), x ∈ H
source
theorem subgroup.eq_top_iff' {G : Type u_1} [group G] (H : subgroup G) :
H = ⊤ ↔ ∀ (x : G), x ∈ H
source
def add_subgroup.closure {G : Type u_1} [add_group G] (k : set G) :
add_subgroup G

The add_subgroup generated by a set

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

The subgroup generated by a set.

Equations
source
theorem subgroup.mem_closure {G : Type u_1} [group G] {k : set G} {x : G} :
x ∈ subgroup.closure k ↔ ∀ (K : subgroup G), k ⊆ ↑K → x ∈ K
source
theorem add_subgroup.mem_closure {G : Type u_1} [add_group G] {k : set G} {x : G} :
x ∈ add_subgroup.closure k ↔ ∀ (K : add_subgroup G), k ⊆ ↑K → x ∈ K
source
@[simp]
theorem subgroup.subset_closure {G : Type u_1} [group G] {k : set G} :
k ⊆ ↑(subgroup.closure k)

The subgroup generated by a set includes the set.

source
@[simp]
theorem add_subgroup.subset_closure {G : Type u_1} [add_group G] {k : set G} :
k ⊆ ↑(add_subgroup.closure k)

The add_subgroup generated by a set includes the set.

source
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
source
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
source
@[simp]
theorem subgroup.closure_le {G : Type u_1} [group G] (K : subgroup G) {k : set G} :
subgroup.closure k ≤ K ↔ k ⊆ ↑K

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

source
@[simp]
theorem add_subgroup.closure_le {G : Type u_1} [add_group G] (K : add_subgroup G) {k : set G} :
add_subgroup.closure k ≤ K ↔ k ⊆ ↑K

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

source
theorem subgroup.closure_eq_of_le {G : Type u_1} [group G] (K : subgroup G) {k : set G} (h₁ : k ⊆ ↑K) (h₂ : K ≤ subgroup.closure k) :
subgroup.closure k = K
source
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) :
add_subgroup.closure k = K
source
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.

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

source
theorem subgroup.closure_induction' {G : Type u_1} [group G] (k : set G) {p : ↥(subgroup.closure k) → Prop} (Hk : ∀ (x : G) (h : x ∈ k), p ⟨x, _⟩) (H1 : p 1) (Hmul : ∀ (x y : ↥(subgroup.closure k)), p x → p y → p (x * y)) (Hinv : ∀ (x : ↥(subgroup.closure k)), p x → p x⁻¹) (x : ↥(subgroup.closure k)) :
p x

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

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

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

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

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

source
def add_subgroup.gi (G : Type u_1) [add_group G] :
galois_insertion add_subgroup.closure coe

closure forms a Galois insertion with the coercion to set.

Equations
source
def subgroup.gi (G : Type u_1) [group G] :
galois_insertion subgroup.closure coe

closure forms a Galois insertion with the coercion to set.

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

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

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

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

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

Closure of a subgroup K equals K.

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

Additive closure of an additive subgroup K equals K

source
@[simp]
theorem add_subgroup.closure_empty {G : Type u_1} [add_group G] :
add_subgroup.closure ∅ = ⊥
source
@[simp]
theorem subgroup.closure_empty {G : Type u_1} [group G] :
subgroup.closure ∅ = ⊥
source
@[simp]
theorem add_subgroup.closure_univ {G : Type u_1} [add_group G] :
add_subgroup.closure set.univ = ⊤
source
@[simp]
theorem subgroup.closure_univ {G : Type u_1} [group G] :
subgroup.closure set.univ = ⊤
source
theorem subgroup.closure_union {G : Type u_1} [group G] (s t : set G) :
subgroup.closure (s ∪ t) = subgroup.closure s ⊔ subgroup.closure t
source
theorem add_subgroup.closure_union {G : Type u_1} [add_group G] (s t : set G) :
add_subgroup.closure (s ∪ t) = add_subgroup.closure s ⊔ add_subgroup.closure t
source
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)
source
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)
source
theorem subgroup.closure_eq_bot_iff (G : Type u_1) [group G] (S : set G) :
subgroup.closure S = ⊥ ↔ S ⊆ {1}
source
theorem add_subgroup.closure_eq_bot_iff (G : Type u_1) [add_group G] (S : set G) :
add_subgroup.closure S = ⊥ ↔ S ⊆ {0}
source
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.

source
theorem subgroup.closure_singleton_one {G : Type u_1} [group G] :
subgroup.closure {1} = ⊥
source
@[simp]
theorem subgroup.inv_subset_closure {G : Type u_1} [group G] (S : set G) :
S⁻¹ ⊆ ↑(subgroup.closure S)
source
@[simp]
theorem add_subgroup.neg_subset_closure {G : Type u_1} [add_group G] (S : set G) :
-S ⊆ ↑(add_subgroup.closure S)
source
@[simp]
theorem subgroup.closure_inv {G : Type u_1} [group G] (S : set G) :
subgroup.closure S⁻¹ = subgroup.closure S
source
@[simp]
theorem add_subgroup.closure_neg {G : Type u_1} [add_group G] (S : set G) :
add_subgroup.closure (-S) = add_subgroup.closure S
source
theorem add_subgroup.closure_to_add_submonoid {G : Type u_1} [add_group G] (S : set G) :
(add_subgroup.closure S).to_add_submonoid = add_submonoid.closure (S ∪ -S)
source
theorem subgroup.closure_to_submonoid {G : Type u_1} [group G] (S : set G) :
(subgroup.closure S).to_submonoid = submonoid.closure (S ∪ S⁻¹)
source
theorem subgroup.closure_induction'' {G : Type u_1} [group G] {k : set G} {p : G → Prop} {x : G} (h : x ∈ subgroup.closure k) (Hk : ∀ (x : G), x ∈ k → p x) (Hk_inv : ∀ (x : G), x ∈ k → p x⁻¹) (H1 : p 1) (Hmul : ∀ (x y : G), p x → p y → p (x * y)) :
p x

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

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

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

source
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
source
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
source
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)
source
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)
source
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 ∈ Sup K ↔ ∃ (s : add_subgroup G) (H : s ∈ K), x ∈ s
source
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 ∈ Sup K ↔ ∃ (s : subgroup G) (H : s ∈ K), x ∈ s
source
def subgroup.comap {G : Type u_1} [group G] {N : Type u_2} [group N] (f : G →* N) (H : subgroup N) :
subgroup G

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

Equations
source
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) :
add_subgroup G

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

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

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

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

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

Equations
source
@[simp]
theorem add_subgroup.coe_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (K : add_subgroup G) :
↑(add_subgroup.map f K) = ⇑f '' ↑K
source
@[simp]
theorem subgroup.coe_map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (K : subgroup G) :
↑(subgroup.map f K) = ⇑f '' ↑K
source
@[simp]
theorem add_subgroup.mem_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K : add_subgroup G} {y : N} :
y ∈ add_subgroup.map f K ↔ ∃ (x : G) (H : x ∈ K), ⇑f x = y
source
@[simp]
theorem subgroup.mem_map {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K : subgroup G} {y : N} :
y ∈ subgroup.map f K ↔ ∃ (x : G) (H : x ∈ K), ⇑f x = y
source
theorem add_subgroup.mem_map_of_mem {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) {K : add_subgroup G} {x : G} (hx : x ∈ K) :
⇑f x ∈ add_subgroup.map f K
source
theorem subgroup.mem_map_of_mem {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) {K : subgroup G} {x : G} (hx : x ∈ K) :
⇑f x ∈ subgroup.map f K
source
theorem add_subgroup.apply_coe_mem_map {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) (K : add_subgroup G) (x : ↥K) :
⇑f ↑x ∈ add_subgroup.map f K
source
theorem subgroup.apply_coe_mem_map {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (K : subgroup G) (x : ↥K) :
⇑f ↑x ∈ subgroup.map f K
source
theorem add_subgroup.map_mono {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K K' : add_subgroup G} :
K ≤ K' → add_subgroup.map f K ≤ add_subgroup.map f K'
source
theorem subgroup.map_mono {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K K' : subgroup G} :
K ≤ K' → subgroup.map f K ≤ subgroup.map f K'
source
@[simp]
theorem add_subgroup.map_id {G : Type u_1} [add_group G] (K : add_subgroup G) :
add_subgroup.map (add_monoid_hom.id G) K = K
source
@[simp]
theorem subgroup.map_id {G : Type u_1} [group G] (K : subgroup G) :
subgroup.map (monoid_hom.id G) K = K
source
theorem add_subgroup.map_map {G : Type u_1} [add_group G] (K : add_subgroup G) {N : Type u_3} [add_group N] {P : Type u_4} [add_group P] (g : N →+ P) (f : G →+ N) :
add_subgroup.map g (add_subgroup.map f K) = add_subgroup.map (g.comp f) K
source
theorem subgroup.map_map {G : Type u_1} [group G] (K : subgroup G) {N : Type u_3} [group N] {P : Type u_4} [group P] (g : N →* P) (f : G →* N) :
subgroup.map g (subgroup.map f K) = subgroup.map (g.comp f) K
source
theorem subgroup.mem_map_equiv {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G ≃* N} {K : subgroup G} {x : N} :
x ∈ subgroup.map f.to_monoid_hom K ↔ ⇑(f.symm) x ∈ K
source
theorem add_subgroup.mem_map_equiv {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G ≃+ N} {K : add_subgroup G} {x : N} :
x ∈ add_subgroup.map f.to_add_monoid_hom K ↔ ⇑(f.symm) x ∈ K
source
theorem subgroup.mem_map_iff_mem {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} (hf : function.injective ⇑f) {K : subgroup G} {x : G} :
⇑f x ∈ subgroup.map f K ↔ x ∈ K
source
theorem add_subgroup.mem_map_iff_mem {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} (hf : function.injective ⇑f) {K : add_subgroup G} {x : G} :
⇑f x ∈ add_subgroup.map f K ↔ x ∈ K
source
theorem subgroup.map_equiv_eq_comap_symm {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G ≃* N) (K : subgroup G) :
subgroup.map f.to_monoid_hom K = subgroup.comap f.symm.to_monoid_hom K
source
theorem add_subgroup.map_equiv_eq_comap_symm {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G ≃+ N) (K : add_subgroup G) :
add_subgroup.map f.to_add_monoid_hom K = add_subgroup.comap f.symm.to_add_monoid_hom K
source
theorem subgroup.comap_equiv_eq_map_symm {G : Type u_1} [group G] {N : Type u_3} [group N] (f : N ≃* G) (K : subgroup G) :
subgroup.comap f.to_monoid_hom K = subgroup.map f.symm.to_monoid_hom K
source
theorem add_subgroup.comap_equiv_eq_map_symm {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : N ≃+ G) (K : add_subgroup G) :
add_subgroup.comap f.to_add_monoid_hom K = add_subgroup.map f.symm.to_add_monoid_hom K
source
theorem add_subgroup.map_le_iff_le_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {f : G →+ N} {K : add_subgroup G} {H : add_subgroup N} :
add_subgroup.map f K ≤ H ↔ K ≤ add_subgroup.comap f H
source
theorem subgroup.map_le_iff_le_comap {G : Type u_1} [group G] {N : Type u_3} [group N] {f : G →* N} {K : subgroup G} {H : subgroup N} :
subgroup.map f K ≤ H ↔ K ≤ subgroup.comap f H
source
theorem subgroup.gc_map_comap {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
galois_connection (subgroup.map f) (subgroup.comap f)
source
theorem add_subgroup.gc_map_comap {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
galois_connection (add_subgroup.map f) (add_subgroup.comap f)
source
theorem add_subgroup.map_sup {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup G) (f : G →+ N) :
add_subgroup.map f (H ⊔ K) = add_subgroup.map f H ⊔ add_subgroup.map f K
source
theorem subgroup.map_sup {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup G) (f : G →* N) :
subgroup.map f (H ⊔ K) = subgroup.map f H ⊔ subgroup.map f K
source
theorem add_subgroup.map_supr {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι → add_subgroup G) :
add_subgroup.map f (supr s) = ⨆ (i : ι), add_subgroup.map f (s i)
source
theorem subgroup.map_supr {G : Type u_1} [group G] {N : Type u_3} [group N] {ι : Sort u_2} (f : G →* N) (s : ι → subgroup G) :
subgroup.map f (supr s) = ⨆ (i : ι), subgroup.map f (s i)
source
theorem add_subgroup.comap_sup_comap_le {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup N) (f : G →+ N) :
add_subgroup.comap f H ⊔ add_subgroup.comap f K ≤ add_subgroup.comap f (H ⊔ K)
source
theorem subgroup.comap_sup_comap_le {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup N) (f : G →* N) :
subgroup.comap f H ⊔ subgroup.comap f K ≤ subgroup.comap f (H ⊔ K)
source
theorem add_subgroup.supr_comap_le {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι → add_subgroup N) :
(⨆ (i : ι), add_subgroup.comap f (s i)) ≤ add_subgroup.comap f (supr s)
source
theorem subgroup.supr_comap_le {G : Type u_1} [group G] {N : Type u_3} [group N] {ι : Sort u_2} (f : G →* N) (s : ι → subgroup N) :
(⨆ (i : ι), subgroup.comap f (s i)) ≤ subgroup.comap f (supr s)
source
theorem add_subgroup.comap_inf {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup N) (f : G →+ N) :
add_subgroup.comap f (H ⊓ K) = add_subgroup.comap f H ⊓ add_subgroup.comap f K
source
theorem subgroup.comap_inf {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup N) (f : G →* N) :
subgroup.comap f (H ⊓ K) = subgroup.comap f H ⊓ subgroup.comap f K
source
theorem subgroup.comap_infi {G : Type u_1} [group G] {N : Type u_3} [group N] {ι : Sort u_2} (f : G →* N) (s : ι → subgroup N) :
subgroup.comap f (infi s) = ⨅ (i : ι), subgroup.comap f (s i)
source
theorem add_subgroup.comap_infi {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {ι : Sort u_2} (f : G →+ N) (s : ι → add_subgroup N) :
add_subgroup.comap f (infi s) = ⨅ (i : ι), add_subgroup.comap f (s i)
source
theorem add_subgroup.map_inf_le {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup G) (f : G →+ N) :
add_subgroup.map f (H ⊓ K) ≤ add_subgroup.map f H ⊓ add_subgroup.map f K
source
theorem subgroup.map_inf_le {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup G) (f : G →* N) :
subgroup.map f (H ⊓ K) ≤ subgroup.map f H ⊓ subgroup.map f K
source
theorem subgroup.map_inf_eq {G : Type u_1} [group G] {N : Type u_3} [group N] (H K : subgroup G) (f : G →* N) (hf : function.injective ⇑f) :
subgroup.map f (H ⊓ K) = subgroup.map f H ⊓ subgroup.map f K
source
theorem add_subgroup.map_inf_eq {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H K : add_subgroup G) (f : G →+ N) (hf : function.injective ⇑f) :
add_subgroup.map f (H ⊓ K) = add_subgroup.map f H ⊓ add_subgroup.map f K
source
@[simp]
theorem add_subgroup.map_bot {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
add_subgroup.map f ⊥ = ⊥
source
@[simp]
theorem subgroup.map_bot {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
subgroup.map f ⊥ = ⊥
source
@[simp]
theorem subgroup.comap_top {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) :
subgroup.comap f ⊤ = ⊤
source
@[simp]
theorem add_subgroup.comap_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (f : G →+ N) :
add_subgroup.comap f ⊤ = ⊤
source
@[simp]
theorem add_subgroup.comap_subtype_inf_left {G : Type u_1} [add_group G] {H K : add_subgroup G} :
add_subgroup.comap H.subtype (H ⊓ K) = add_subgroup.comap H.subtype K
source
@[simp]
theorem subgroup.comap_subtype_inf_left {G : Type u_1} [group G] {H K : subgroup G} :
subgroup.comap H.subtype (H ⊓ K) = subgroup.comap H.subtype K
source
@[simp]
theorem add_subgroup.comap_subtype_inf_right {G : Type u_1} [add_group G] {H K : add_subgroup G} :
add_subgroup.comap K.subtype (H ⊓ K) = add_subgroup.comap K.subtype H
source
@[simp]
theorem subgroup.comap_subtype_inf_right {G : Type u_1} [group G] {H K : subgroup G} :
subgroup.comap K.subtype (H ⊓ K) = subgroup.comap K.subtype H
source
@[simp]
theorem add_subgroup.comap_subtype_equiv_of_le_symm_apply_coe_coe {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) (g : ↥H) :
↑↑(⇑((add_subgroup.comap_subtype_equiv_of_le h).symm) g) = g.val
source
@[simp]
theorem add_subgroup.comap_subtype_equiv_of_le_apply_coe {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) (g : ↥(add_subgroup.comap K.subtype H)) :
↑(⇑(add_subgroup.comap_subtype_equiv_of_le h) g) = ↑(g.val)
source
def subgroup.comap_subtype_equiv_of_le {G : Type u_1} [group G] {H K : subgroup G} (h : H ≤ K) :
↥(subgroup.comap K.subtype H) ≃* ↥H

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

Equations
source
def add_subgroup.comap_subtype_equiv_of_le {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) :
↥(add_subgroup.comap K.subtype H) ≃+ ↥H

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

Equations
source
@[simp]
theorem subgroup.comap_subtype_equiv_of_le_apply_coe {G : Type u_1} [group G] {H K : subgroup G} (h : H ≤ K) (g : ↥(subgroup.comap K.subtype H)) :
↑(⇑(subgroup.comap_subtype_equiv_of_le h) g) = ↑(g.val)
source
@[simp]
theorem subgroup.comap_subtype_equiv_of_le_symm_apply_coe_coe {G : Type u_1} [group G] {H K : subgroup G} (h : H ≤ K) (g : ↥H) :
↑↑(⇑((subgroup.comap_subtype_equiv_of_le h).symm) g) = g.val
source
def add_subgroup.add_subgroup_of {G : Type u_1} [add_group G] (H K : add_subgroup G) :
add_subgroup ↥K

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

Equations
source
def subgroup.subgroup_of {G : Type u_1} [group G] (H K : subgroup G) :
subgroup ↥K

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

Equations
source
theorem add_subgroup.coe_add_subgroup_of {G : Type u_1} [add_group G] (H K : add_subgroup G) :
↑(H.add_subgroup_of K) = ⇑(K.subtype) ⁻¹' ↑H
source
theorem subgroup.coe_subgroup_of {G : Type u_1} [group G] (H K : subgroup G) :
↑(H.subgroup_of K) = ⇑(K.subtype) ⁻¹' ↑H
source
theorem subgroup.mem_subgroup_of {G : Type u_1} [group G] {H K : subgroup G} {h : ↥K} :
h ∈ H.subgroup_of K ↔ ↑h ∈ H
source
theorem add_subgroup.mem_add_subgroup_of {G : Type u_1} [add_group G] {H K : add_subgroup G} {h : ↥K} :
h ∈ H.add_subgroup_of K ↔ ↑h ∈ H
source
theorem add_subgroup.add_subgroup_of_map_subtype {G : Type u_1} [add_group G] (H K : add_subgroup G) :
add_subgroup.map K.subtype (H.add_subgroup_of K) = H ⊓ K
source
theorem subgroup.subgroup_of_map_subtype {G : Type u_1} [group G] (H K : subgroup G) :
subgroup.map K.subtype (H.subgroup_of K) = H ⊓ K
source
@[simp]
theorem add_subgroup.bot_add_subgroup_of {G : Type u_1} [add_group G] (H : add_subgroup G) :
⊥.add_subgroup_of H = ⊥
source
@[simp]
theorem subgroup.bot_subgroup_of {G : Type u_1} [group G] (H : subgroup G) :
⊥.subgroup_of H = ⊥
source
@[simp]
theorem subgroup.top_subgroup_of {G : Type u_1} [group G] (H : subgroup G) :
⊤.subgroup_of H = ⊤
source
@[simp]
theorem add_subgroup.top_add_subgroup_of {G : Type u_1} [add_group G] (H : add_subgroup G) :
⊤.add_subgroup_of H = ⊤
source
theorem add_subgroup.add_subgroup_of_bot_eq_bot {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.add_subgroup_of ⊥ = ⊥
source
theorem subgroup.subgroup_of_bot_eq_bot {G : Type u_1} [group G] (H : subgroup G) :
H.subgroup_of ⊥ = ⊥
source
theorem add_subgroup.add_subgroup_of_bot_eq_top {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.add_subgroup_of ⊥ = ⊤
source
theorem subgroup.subgroup_of_bot_eq_top {G : Type u_1} [group G] (H : subgroup G) :
H.subgroup_of ⊥ = ⊤
source
@[simp]
theorem subgroup.subgroup_of_self {G : Type u_1} [group G] (H : subgroup G) :
H.subgroup_of H = ⊤
source
@[simp]
theorem add_subgroup.add_subgroup_of_self {G : Type u_1} [add_group G] (H : add_subgroup G) :
H.add_subgroup_of H = ⊤
source
def add_subgroup.prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :
add_subgroup (G × N)

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

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

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

Equations
source
theorem subgroup.coe_prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) :
↑(H.prod K) = ↑H.prod ↑K
source
theorem add_subgroup.coe_prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :
↑(H.prod K) = ↑H.prod ↑K
source
theorem add_subgroup.mem_prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] {H : add_subgroup G} {K : add_subgroup N} {p : G × N} :
p ∈ H.prod K ↔ p.fst ∈ H ∧ p.snd ∈ K
source
theorem subgroup.mem_prod {G : Type u_1} [group G] {N : Type u_3} [group N] {H : subgroup G} {K : subgroup N} {p : G × N} :
p ∈ H.prod K ↔ p.fst ∈ H ∧ p.snd ∈ K
source
theorem add_subgroup.prod_mono {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :
(has_le.le ⇒ has_le.le ⇒ has_le.le) add_subgroup.prod add_subgroup.prod
source
theorem subgroup.prod_mono {G : Type u_1} [group G] {N : Type u_3} [group N] :
(has_le.le ⇒ has_le.le ⇒ has_le.le) subgroup.prod subgroup.prod
source
theorem subgroup.prod_mono_right {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup G) :
monotone (λ (t : subgroup N), K.prod t)
source
theorem add_subgroup.prod_mono_right {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (K : add_subgroup G) :
monotone (λ (t : add_subgroup N), K.prod t)
source
theorem add_subgroup.prod_mono_left {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup N) :
monotone (λ (K : add_subgroup G), K.prod H)
source
theorem subgroup.prod_mono_left {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup N) :
monotone (λ (K : subgroup G), K.prod H)
source
theorem add_subgroup.prod_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (K : add_subgroup G) :
K.prod ⊤ = add_subgroup.comap (add_monoid_hom.fst G N) K
source
theorem subgroup.prod_top {G : Type u_1} [group G] {N : Type u_3} [group N] (K : subgroup G) :
K.prod ⊤ = subgroup.comap (monoid_hom.fst G N) K
source
theorem add_subgroup.top_prod {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup N) :
⊤.prod H = add_subgroup.comap (add_monoid_hom.snd G N) H
source
theorem subgroup.top_prod {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup N) :
⊤.prod H = subgroup.comap (monoid_hom.snd G N) H
source
@[simp]
theorem subgroup.top_prod_top {G : Type u_1} [group G] {N : Type u_3} [group N] :
⊤.prod ⊤ = ⊤
source
@[simp]
theorem add_subgroup.top_prod_top {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :
⊤.prod ⊤ = ⊤
source
theorem subgroup.bot_prod_bot {G : Type u_1} [group G] {N : Type u_3} [group N] :
⊥.prod ⊥ = ⊥
source
theorem add_subgroup.bot_sum_bot {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] :
⊥.prod ⊥ = ⊥
source
def subgroup.prod_equiv {G : Type u_1} [group G] {N : Type u_3} [group N] (H : subgroup G) (K : subgroup N) :
↥(H.prod K) ≃* ↥H × ↥K

Product of subgroups is isomorphic to their product as groups.

Equations
source
def add_subgroup.prod_equiv {G : Type u_1} [add_group G] {N : Type u_3} [add_group N] (H : add_subgroup G) (K : add_subgroup N) :
↥(H.prod K) ≃+ ↥H × ↥K

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

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

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

Instances
source
@[class]
structure add_subgroup.normal {A : Type u_2} [add_group A] (H : add_subgroup A) :
Prop
  • conj_mem : ∀ (n : A), n ∈ H → ∀ (g : A), g + n + -g ∈ H

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

Instances
source
@[instance]
def subgroup.normal_of_comm {G : Type u_1} [comm_group G] (H : subgroup G) :
H.normal
source
@[instance]
def add_subgroup.normal_of_comm {G : Type u_1} [add_comm_group G] (H : add_subgroup G) :
H.normal
source
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
source
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
source
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
source
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
source
@[instance]
def add_subgroup.bot_normal {G : Type u_1} [add_group G] :
⊥.normal
source
@[instance]
def subgroup.bot_normal {G : Type u_1} [group G] :
⊥.normal
source
@[instance]
def subgroup.top_normal {G : Type u_1} [group G] :
⊤.normal
source
@[instance]
def add_subgroup.top_normal {G : Type u_1} [add_group G] :
⊤.normal
source
def add_subgroup.center (G : Type u_1) [add_group G] :
add_subgroup G

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

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

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

Equations
source
theorem subgroup.coe_center (G : Type u_1) [group G] :
↑(subgroup.center G) = set.center G
source
theorem add_subgroup.coe_center (G : Type u_1) [add_group G] :
↑(add_subgroup.center G) = set.add_center G
source
@[simp]
theorem add_subgroup.center_to_add_submonoid (G : Type u_1) [add_group G] :
(add_subgroup.center G).to_add_submonoid = add_submonoid.center G
source
@[simp]
theorem subgroup.center_to_submonoid (G : Type u_1) [group G] :
(subgroup.center G).to_submonoid = submonoid.center G
source
theorem subgroup.mem_center_iff {G : Type u_1} [group G] {z : G} :
z ∈ subgroup.center G ↔ ∀ (g : G), g * z = z * g
source
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
source
@[instance]
def subgroup.decidable_mem_center {G : Type u_1} [group G] [decidable_eq G] [fintype G] :
decidable_pred (λ (_x : G), _x ∈ subgroup.center G)
Equations
source
@[instance]
def add_subgroup.center_normal {G : Type u_1} [add_group G] :
(add_subgroup.center G).normal
source
@[instance]
def subgroup.center_normal {G : Type u_1} [group G] :
(subgroup.center G).normal
source
def add_subgroup.normalizer {G : Type u_1} [add_group G] (H : add_subgroup G) :
add_subgroup G

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

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

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

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

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

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

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

Equations
source
theorem subgroup.mem_normalizer_fintype {G : Type u_1} [group G] {S : set G} [fintype ↥S] {x : G} (h : ∀ (n : G), n ∈ S → (x * n) * x⁻¹ ∈ S) :
x ∈ subgroup.set_normalizer S
source
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 ∈ H ↔ g + n + -g ∈ H
source
theorem subgroup.mem_normalizer_iff {G : Type u_1} [group G] {H : subgroup G} {g : G} :
g ∈ H.normalizer ↔ ∀ (n : G), n ∈ H ↔ (g * n) * g⁻¹ ∈ H
source
theorem add_subgroup.le_normalizer {G : Type u_1} [add_group G] {H : add_subgroup G} :
H ≤ H.normalizer
source
theorem subgroup.le_normalizer {G : Type u_1} [group G] {H : subgroup G} :
H ≤ H.