group_theory.subgroup.basic

source

@[class]

structure inv_mem_class (S : Type u_4) (G : Type u_5) [has_inv G] [set_like S G] :

Prop

inv_mem : ∀ {s : S} {x : G}, x ∈ s → x⁻¹ ∈ s

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

Instances of this typeclass

source

@[class]

structure neg_mem_class (S : Type u_4) (G : Type u_5) [has_neg G] [set_like S G] :

Prop

neg_mem : ∀ {s : S} {x : G}, x ∈ s → -x ∈ s

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

Instances of this typeclass

source

@[class]

structure subgroup_class (S : Type u_4) (G : Type u_5) [div_inv_monoid G] [set_like S G] :

Prop

to_submonoid_class : submonoid_class S G
to_inv_mem_class : inv_mem_class S G

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

Instances of this typeclass

source

@[class]

structure add_subgroup_class (S : Type u_4) (G : Type u_5) [sub_neg_monoid G] [set_like S G] :

Prop

to_add_submonoid_class : add_submonoid_class S G
to_neg_mem_class : neg_mem_class S G

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

Instances of this typeclass

source

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.

source

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.

source

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

source

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

source

@[simp]

theorem neg_mem_iff {G : Type u_1} [add_group G] {S : Type u_5} {H : S} [set_like S G] [hSG : add_subgroup_class S G] {x : G} :

-x ∈ H ↔ x ∈ H

source

@[simp]

theorem inv_mem_iff {G : Type u_1} [group G] {S : Type u_5} {H : S} [set_like S G] [hSG : subgroup_class S G] {x : G} :

x⁻¹ ∈ H ↔ x ∈ H

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

has_neg ↥H

An additive subgroup of a add_group inherits an inverse.

Equations

add_subgroup_class.has_neg = {neg := λ (a : ↥H), ⟨-↑a, _⟩}

source

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

has_inv ↥H

A subgroup of a group inherits an inverse.

Equations

subgroup_class.has_inv = {inv := λ (a : ↥H), ⟨(↑a)⁻¹, _⟩}

source

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

has_div ↥H

A subgroup of a group inherits a division

Equations

subgroup_class.has_div = {div := λ (a b : ↥H), ⟨↑a / ↑b, _⟩}

source

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

has_sub ↥H

An additive subgroup of an add_group inherits a subtraction.

Equations

add_subgroup_class.has_sub = {sub := λ (a b : ↥H), ⟨↑a - ↑b, _⟩}

source

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

has_smul ℤ ↥H

An additive subgroup of an add_group inherits an integer scaling.

Equations

add_subgroup_class.has_zsmul = {smul := λ (n : ℤ) (a : ↥H), ⟨n • ↑a, _⟩}

source

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

has_pow ↥H ℤ

A subgroup of a group inherits an integer power.

Equations

subgroup_class.has_zpow = {pow := λ (a : ↥H) (n : ℤ), ⟨↑a ^ n, _⟩}

source

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

↑-x = -↑x

source

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

↑x⁻¹ = (↑x)⁻¹

source

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

source

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

source

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

group ↥H

A subgroup of a group inherits a group structure.

Equations

subgroup_class.to_group H = function.injective.group coe _ _ _ _ _ _ _

source

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

add_group ↥H

An additive subgroup of an add_group inherits an add_group structure.

Equations

add_subgroup_class.to_add_group H = function.injective.add_group coe _ _ _ _ _ _ _

source

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

comm_group ↥H

A subgroup of a comm_group is a comm_group.

Equations

subgroup_class.to_comm_group H = function.injective.comm_group coe _ _ _ _ _ _ _

source

@[protected, instance]

def add_subgroup_class.to_add_comm_group {S : Type u_5} (H : S) {G : Type u_1} [add_comm_group G] [set_like S G] [add_subgroup_class S G] :

add_comm_group ↥H

An additive subgroup of an add_comm_group is an add_comm_group.

Equations

add_subgroup_class.to_add_comm_group H = function.injective.add_comm_group coe _ _ _ _ _ _ _

source

@[protected, instance]

def add_subgroup_class.to_ordered_add_comm_group {S : Type u_5} (H : S) {G : Type u_1} [ordered_add_comm_group G] [set_like S G] [add_subgroup_class S G] :

ordered_add_comm_group ↥H

An additive subgroup of an add_ordered_comm_group is an add_ordered_comm_group.

Equations

add_subgroup_class.to_ordered_add_comm_group H = function.injective.ordered_add_comm_group coe _ _ _ _ _ _ _

source

@[protected, instance]

def subgroup_class.to_ordered_comm_group {S : Type u_5} (H : S) {G : Type u_1} [ordered_comm_group G] [set_like S G] [subgroup_class S G] :

ordered_comm_group ↥H

A subgroup of an ordered_comm_group is an ordered_comm_group.

Equations

subgroup_class.to_ordered_comm_group H = function.injective.ordered_comm_group coe _ _ _ _ _ _ _

source

@[protected, instance]

def add_subgroup_class.to_linear_ordered_add_comm_group {S : Type u_5} (H : S) {G : Type u_1} [linear_ordered_add_comm_group G] [set_like S G] [add_subgroup_class S G] :

linear_ordered_add_comm_group ↥H

An additive subgroup of a linear_ordered_add_comm_group is a linear_ordered_add_comm_group.

Equations

add_subgroup_class.to_linear_ordered_add_comm_group H = function.injective.linear_ordered_add_comm_group coe _ _ _ _ _ _ _ _ _

source

@[protected, instance]

def subgroup_class.to_linear_ordered_comm_group {S : Type u_5} (H : S) {G : Type u_1} [linear_ordered_comm_group G] [set_like S G] [subgroup_class S G] :

linear_ordered_comm_group ↥H

A subgroup of a linear_ordered_comm_group is a linear_ordered_comm_group.

Equations

subgroup_class.to_linear_ordered_comm_group H = function.injective.linear_ordered_comm_group coe _ _ _ _ _ _ _ _ _

source

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

↥H →+ G

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

Equations

add_subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

source

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

↥H →* G

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

Equations

subgroup_class.subtype H = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}

source

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

⇑(add_subgroup_class.subtype H) = coe

source

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

⇑(subgroup_class.subtype H) = coe

source

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

source

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

source

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

source

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

source

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

↥H →+ ↥K

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

Equations

add_subgroup_class.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _

source

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

↥H →* ↥K

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

Equations

subgroup_class.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _

source

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

⇑(add_subgroup_class.inclusion le_rfl) x = x

source

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

⇑(subgroup_class.inclusion le_rfl) x = x

source

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

⇑(add_subgroup_class.inclusion h) ⟨x, hx⟩ = ⟨x, _⟩

source

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

⇑(subgroup_class.inclusion h) ⟨x, hx⟩ = ⟨x, _⟩

source

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

⇑(subgroup_class.inclusion h) ⟨↑x, hx⟩ = x

source

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

⇑(add_subgroup_class.inclusion h) ⟨↑x, hx⟩ = x

source

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

⇑(subgroup_class.inclusion hKL) (⇑(subgroup_class.inclusion hHK) x) = ⇑(subgroup_class.inclusion _) x

source

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

↑(⇑(add_subgroup_class.inclusion h) a) = ↑a

source

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

↑(⇑(subgroup_class.inclusion h) a) = ↑a

source

@[simp]

theorem add_subgroup_class.subtype_comp_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} (hH : H ≤ K) :

(add_subgroup_class.subtype K).comp (add_subgroup_class.inclusion hH) = add_subgroup_class.subtype H

source

@[simp]

theorem subgroup_class.subtype_comp_inclusion {G : Type u_1} [group G] {S : Type u_5} [set_like S G] [hSG : subgroup_class S G] {H K : S} (hH : H ≤ K) :

(subgroup_class.subtype K).comp (subgroup_class.inclusion hH) = subgroup_class.subtype H

source

def subgroup.to_submonoid {G : Type u_4} [group G] (self : subgroup G) :

submonoid G

Reinterpret a subgroup as a submonoid.

source

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

Type u_4

carrier : set G
mul_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
one_mem' : 1 ∈ self.carrier
inv_mem' : ∀ {x : G}, x ∈ self.carrier → x⁻¹ ∈ self.carrier

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

Instances for subgroup

source

structure add_subgroup (G : Type u_4) [add_group G] :

Type u_4

carrier : set G
add_mem' : ∀ {a b : G}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
zero_mem' : 0 ∈ self.carrier
neg_mem' : ∀ {x : G}, x ∈ self.carrier → -x ∈ self.carrier

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

Instances for add_subgroup

source

def add_subgroup.to_add_submonoid {G : Type u_4} [add_group G] (self : add_subgroup G) :

add_submonoid G

Reinterpret an add_subgroup as an add_submonoid.

source

@[protected, instance]

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

set_like (subgroup G) G

Equations

subgroup.set_like = {coe := subgroup.carrier _inst_1, coe_injective' := _}

source

@[protected, instance]

def add_subgroup.set_like {G : Type u_1} [add_group G] :

set_like (add_subgroup G) G

Equations

add_subgroup.set_like = {coe := add_subgroup.carrier _inst_1, coe_injective' := _}

source

@[protected, instance]

def add_subgroup.add_subgroup_class {G : Type u_1} [add_group G] :

add_subgroup_class (add_subgroup G) G

source

@[protected, instance]

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

subgroup_class (subgroup G) G

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 : ∀ {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

source

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

source

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

source

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

source

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

source

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

source

def subgroup.simps.coe {G : Type u_1} [group G] (S : subgroup G) :

set G

See Note [custom simps projection]

Equations

subgroup.simps.coe S = ↑S

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

add_subgroup.simps.coe S = ↑S

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

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

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

subgroup.to_add_subgroup = {to_equiv := {to_fun := λ (S : subgroup G), {carrier := (⇑submonoid.to_add_submonoid S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, inv_fun := λ (S : add_subgroup (additive G)), {carrier := (⇑add_submonoid.to_submonoid' S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}

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

@[reducible]

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_3} [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

add_subgroup.to_subgroup = {to_equiv := {to_fun := λ (S : add_subgroup A), {carrier := (⇑add_submonoid.to_submonoid S.to_add_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}, inv_fun := λ (S : subgroup (multiplicative A)), {carrier := (⇑submonoid.to_add_submonoid' S.to_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem add_subgroup.to_subgroup_apply_coe {A : Type u_3} [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_3} [add_group A] (S : subgroup (multiplicative A)) :

↑(⇑(rel_iso.symm add_subgroup.to_subgroup) S) = (⇑submonoid.to_add_submonoid' S.to_submonoid).carrier

source

@[reducible]

def subgroup.to_add_subgroup' {A : Type u_3} [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

@[protected]

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

K.copy s hs = {carrier := s, mul_mem' := _, one_mem' := _, inv_mem' := _}

source

@[protected]

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

K.copy s hs = {carrier := s, add_mem' := _, zero_mem' := _, neg_mem' := _}

source

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

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

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

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

source

@[protected]

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

1 ∈ H

A subgroup contains the group's 1.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[protected]

theorem add_subgroup.neg_mem_iff {G : Type u_1} [add_group G] (H : add_subgroup G) {x : G} :

-x ∈ H ↔ x ∈ H

source

@[protected]

theorem subgroup.inv_mem_iff {G : Type u_1} [group G] (H : subgroup G) {x : G} :

x⁻¹ ∈ H ↔ x ∈ H

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[protected]

theorem subgroup.pow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x ∈ K) (n : ℕ) :

x ^ n ∈ K

source

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

source

@[protected]

theorem subgroup.zpow_mem {G : Type u_1} [group G] (K : subgroup G) {x : G} (hx : x ∈ K) (n : ℤ) :

x ^ n ∈ K

source

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

source

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

subgroup G

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

Equations

subgroup.of_div s hsn hs = have one_mem : 1 ∈ s, from _, have inv_mem : ∀ (x : G), x ∈ s → x⁻¹ ∈ s, from _, {carrier := s, mul_mem' := _, one_mem' := one_mem, inv_mem' := inv_mem}
_ = _

source

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

add_subgroup G

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

Equations

add_subgroup.of_sub s hsn hs = have one_mem : 0 ∈ s, from _, have inv_mem : ∀ (x : G), x ∈ s → -x ∈ s, from _, {carrier := s, add_mem' := _, zero_mem' := one_mem, neg_mem' := inv_mem}
_ = _

source

@[protected, 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

H.has_mul = H.to_submonoid.has_mul

source

@[protected, 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

H.has_add = H.to_add_submonoid.has_add

source

@[protected, 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

H.has_one = H.to_submonoid.has_one

source

@[protected, 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

H.has_zero = H.to_add_submonoid.has_zero

source

@[protected, 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

H.has_neg = {neg := λ (a : ↥H), ⟨-↑a, _⟩}

source

@[protected, 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

H.has_inv = {inv := λ (a : ↥H), ⟨(↑a)⁻¹, _⟩}

source

@[protected, 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

H.has_div = {div := λ (a b : ↥H), ⟨↑a / ↑b, _⟩}

source

@[protected, 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

H.has_sub = {sub := λ (a b : ↥H), ⟨↑a - ↑b, _⟩}

source

@[protected, instance]

def add_subgroup.has_nsmul {G : Type u_1} [add_group G] {H : add_subgroup G} :

has_smul ℕ ↥H

An add_subgroup of an add_group inherits a natural scaling.

Equations

add_subgroup.has_nsmul = {smul := λ (n : ℕ) (a : ↥H), ⟨n • ↑a, _⟩}

source

@[protected, instance]

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

has_pow ↥H ℕ

A subgroup of a group inherits a natural power

Equations

H.has_npow = {pow := λ (a : ↥H) (n : ℕ), ⟨↑a ^ n, _⟩}

source

@[protected, instance]

def add_subgroup.has_zsmul {G : Type u_1} [add_group G] {H : add_subgroup G} :

has_smul ℤ ↥H

An add_subgroup of an add_group inherits an integer scaling.

Equations

add_subgroup.has_zsmul = {smul := λ (n : ℤ) (a : ↥H), ⟨n • ↑a, _⟩}

source

@[protected, instance]

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

has_pow ↥H ℤ

A subgroup of a group inherits an integer power

Equations

H.has_zpow = {pow := λ (a : ↥H) (n : ℤ), ⟨↑a ^ n, _⟩}

source

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

source

@[simp, norm_cast]

theorem subgroup.coe_mul {G : Type u_1} [group G] (H : subgroup G) (x y : ↥H) :

↑(x * y) = ↑x * ↑y

source

@[simp, norm_cast]

theorem add_subgroup.coe_zero {G : Type u_1} [add_group G] (H : add_subgroup G) :

↑0 = 0

source

@[simp, norm_cast]

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

↑1 = 1

source

@[simp, norm_cast]

theorem add_subgroup.coe_neg {G : Type u_1} [add_group G] (H : add_subgroup G) (x : ↥H) :

↑-x = -↑x

source

@[simp, norm_cast]

theorem subgroup.coe_inv {G : Type u_1} [group G] (H : subgroup G) (x : ↥H) :

↑x⁻¹ = (↑x)⁻¹

source

@[simp, norm_cast]

theorem subgroup.coe_div {G : Type u_1} [group G] (H : subgroup G) (x y : ↥H) :

↑(x / y) = ↑x / ↑y

source

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

source

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

source

@[simp, norm_cast]

theorem subgroup.coe_mk {G : Type u_1} [group G] (H : subgroup G) (x : G) (hx : x ∈ H) :

↑⟨x, hx⟩ = x

source

@[simp, norm_cast]

theorem subgroup.coe_pow {G : Type u_1} [group G] (H : subgroup G) (x : ↥H) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

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

source

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

source

@[simp, norm_cast]

theorem subgroup.coe_zpow {G : Type u_1} [group G] (H : subgroup G) (x : ↥H) (n : ℤ) :

↑(x ^ n) = ↑x ^ n

source

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

source

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

source

@[protected, 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

H.to_group = function.injective.group coe _ _ _ _ _ _ _

source

@[protected, 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

H.to_add_group = function.injective.add_group coe _ _ _ _ _ _ _

source

@[protected, 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

H.to_add_comm_group = function.injective.add_comm_group coe _ _ _ _ _ _ _

source

@[protected, 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

H.to_comm_group = function.injective.comm_group coe _ _ _ _ _ _ _

source

@[protected, 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

H.to_ordered_add_comm_group = function.injective.ordered_add_comm_group coe _ _ _ _ _ _ _

source

@[protected, 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

H.to_ordered_comm_group = function.injective.ordered_comm_group coe _ _ _ _ _ _ _

source

@[protected, 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

H.to_linear_ordered_comm_group = function.injective.linear_ordered_comm_group coe _ _ _ _ _ _ _ _ _

source

@[protected, 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

H.to_linear_ordered_add_comm_group = function.injective.linear_ordered_add_comm_group coe _ _ _ _ _ _ _ _ _

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

H.subtype = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _}

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

H.subtype = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := _}

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

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

function.injective ⇑(H.subtype)

source

theorem add_subgroup.subtype_injective {G : Type u_1} [add_group G] (H : add_subgroup G) :

function.injective ⇑(H.subtype)

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

add_subgroup.inclusion h = add_monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _

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

subgroup.inclusion h = monoid_hom.mk' (λ (x : ↥H), ⟨↑x, _⟩) _

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

theorem add_subgroup.inclusion_injective {G : Type u_1} [add_group G] {H K : add_subgroup G} (h : H ≤ K) :

function.injective ⇑(add_subgroup.inclusion h)

source

theorem subgroup.inclusion_injective {G : Type u_1} [group G] {H K : subgroup G} (h : H ≤ K) :

function.injective ⇑(subgroup.inclusion h)

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

@[protected, 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

add_subgroup.has_top = {top := {carrier := ⊤.carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}

source

@[protected, instance]

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

has_top (subgroup G)

The subgroup G of the group G.

Equations

subgroup.has_top = {top := {carrier := ⊤.carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}}

source

@[simp]

theorem add_subgroup.top_equiv_apply {G : Type u_1} [add_group G] (x : ↥⊤) :

⇑add_subgroup.top_equiv x = ↑x

source

@[simp]

theorem subgroup.top_equiv_symm_apply_coe {G : Type u_1} [group G] (x : G) :

↑(⇑(subgroup.top_equiv.symm) x) = x

source

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

↥⊤ ≃* G

The top subgroup is isomorphic to the group.

This is the group version of submonoid.top_equiv.

Equations

subgroup.top_equiv = submonoid.top_equiv

source

@[simp]

theorem add_subgroup.top_equiv_symm_apply_coe {G : Type u_1} [add_group G] (x : G) :

↑(⇑(add_subgroup.top_equiv.symm) x) = x

source

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

↥⊤ ≃+ G

The top additive subgroup is isomorphic to the additive group.

This is the additive group version of add_submonoid.top_equiv.

Equations

add_subgroup.top_equiv = add_submonoid.top_equiv

source

@[simp]

theorem subgroup.top_equiv_apply {G : Type u_1} [group G] (x : ↥⊤) :

⇑subgroup.top_equiv x = ↑x

source

@[protected, 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

add_subgroup.has_bot = {bot := {carrier := ⊥.carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}

source

@[protected, instance]

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

has_bot (subgroup G)

The trivial subgroup {1} of an group G.

Equations

subgroup.has_bot = {bot := {carrier := ⊥.carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}}

source

@[protected, instance]

def add_subgroup.inhabited {G : Type u_1} [add_group G] :

inhabited (add_subgroup G)

Equations

add_subgroup.inhabited = {default := ⊥}

source

@[protected, instance]

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

inhabited (subgroup G)

Equations

subgroup.inhabited = {default := ⊥}

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

@[protected, instance]

def add_subgroup.has_bot.bot.unique {G : Type u_1} [add_group G] :

unique ↥⊥

Equations

add_subgroup.has_bot.bot.unique = {to_inhabited := {default := 0}, uniq := _}

source

@[protected, instance]

def subgroup.has_bot.bot.unique {G : Type u_1} [group G] :

unique ↥⊥

Equations

subgroup.has_bot.bot.unique = {to_inhabited := {default := 1}, uniq := _}

source

@[simp]

theorem subgroup.top_to_submonoid {G : Type u_1} [group G] :

⊤.to_submonoid = ⊤

source

@[simp]

theorem add_subgroup.top_to_add_submonoid {G : Type u_1} [add_group G] :

⊤.to_add_submonoid = ⊤

source

@[simp]

theorem add_subgroup.bot_to_add_submonoid {G : Type u_1} [add_group G] :

⊥.to_add_submonoid = ⊥

source

@[simp]

theorem subgroup.bot_to_submonoid {G : Type u_1} [group G] :

⊥.to_submonoid = ⊥

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

theorem subgroup.coe_eq_univ {G : Type u_1} [group G] {H : subgroup G} :

↑H = set.univ ↔ H = ⊤

source

theorem add_subgroup.coe_eq_univ {G : Type u_1} [add_group G] {H : add_subgroup G} :

↑H = set.univ ↔ H = ⊤

source

theorem add_subgroup.coe_eq_singleton {G : Type u_1} [add_group G] {H : add_subgroup G} :

(∃ (g : G), ↑H = {g}) ↔ H = ⊥

source

theorem subgroup.coe_eq_singleton {G : Type u_1} [group G] {H : subgroup G} :

(∃ (g : G), ↑H = {g}) ↔ 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

A subgroup is either the trivial subgroup or nontrivial.

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 non-identity 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

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

source

@[protected, instance]

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

has_inf (subgroup G)

The inf of two subgroups is their intersection.

Equations

subgroup.has_inf = {inf := λ (H₁ H₂ : subgroup G), {carrier := (H₁.to_submonoid ⊓ H₂.to_submonoid).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}}

source

@[protected, 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

add_subgroup.has_inf = {inf := λ (H₁ H₂ : add_subgroup G), {carrier := (H₁.to_add_submonoid ⊓ H₂.to_add_submonoid).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}

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

@[protected, instance]

def add_subgroup.has_Inf {G : Type u_1} [add_group G] :

has_Inf (add_subgroup G)

Equations

add_subgroup.has_Inf = {Inf := λ (s : set (add_subgroup G)), {carrier := ((⨅ (S : add_subgroup G) (H : S ∈ s), S.to_add_submonoid).copy (⋂ (S : add_subgroup G) (H : S ∈ s), ↑S) _).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}}

source

@[protected, instance]

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

has_Inf (subgroup G)

Equations

subgroup.has_Inf = {Inf := λ (s : set (subgroup G)), {carrier := ((⨅ (S : subgroup G) (H : S ∈ s), S.to_submonoid).copy (⋂ (S : subgroup G) (H : S ∈ s), ↑S) _).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}}

source

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

source

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

source

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

source

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

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

theorem subgroup.coe_infi {G : Type u_1} [group G] {ι : Sort u_2} {S : ι → subgroup G} :

(↑⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)

source

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

source

@[protected, instance]

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

complete_lattice (subgroup G)

Subgroups of a group form a complete lattice.

Equations

subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (subgroup G) subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

source

@[protected, 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

add_subgroup.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le := complete_lattice.le (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), lt := complete_lattice.lt (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf add_subgroup.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Inf (add_subgroup G) add_subgroup.complete_lattice._proof_1), Inf_le := _, le_Inf := _, top := ⊤, bot := ⊥, le_top := _, bot_le := _}

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

source

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

source

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

source

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

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 ∈ has_Sup.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 ∈ has_Sup.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

@[protected, instance]

def add_subgroup.unique {G : Type u_1} [add_group G] [subsingleton G] :

unique (add_subgroup G)

Equations

add_subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}

source

@[protected, instance]

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

unique (subgroup G)

Equations

subgroup.unique = {to_inhabited := {default := ⊥}, uniq := _}

source

@[protected, instance]

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

nontrivial (subgroup G)

source

@[protected, 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

add_subgroup.closure k = has_Inf.Inf {K : add_subgroup G | k ⊆ ↑K}

Instances for ↥add_subgroup.closure

source

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

subgroup G

The subgroup generated by a set.

Equations

subgroup.closure k = has_Inf.Inf {K : subgroup G | k ⊆ ↑K}

Instances for ↥subgroup.closure

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 : Π (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.

source

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.

source

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.

source

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.

source

@[simp]

theorem subgroup.closure_closure_coe_preimage {G : Type u_1} [group G] {k : set G} :

subgroup.closure (coe ⁻¹' k) = ⊤

source

@[simp]

theorem add_subgroup.closure_closure_coe_preimage {G : Type u_1} [add_group G] {k : set G} :

add_subgroup.closure (coe ⁻¹' k) = ⊤

source

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

comm_group ↥(subgroup.closure k)

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

Equations

subgroup.closure_comm_group_of_comm hcomm = {mul := group.mul (subgroup.closure k).to_group, mul_assoc := _, one := group.one (subgroup.closure k).to_group, one_mul := _, mul_one := _, npow := group.npow (subgroup.closure k).to_group, npow_zero' := _, npow_succ' := _, inv := group.inv (subgroup.closure k).to_group, div := group.div (subgroup.closure k).to_group, div_eq_mul_inv := _, zpow := group.zpow (subgroup.closure k).to_group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

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

add_comm_group ↥(add_subgroup.closure k)

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

Equations

add_subgroup.closure_add_comm_group_of_comm hcomm = {add := add_group.add (add_subgroup.closure k).to_add_group, add_assoc := _, zero := add_group.zero (add_subgroup.closure k).to_add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul (add_subgroup.closure k).to_add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (add_subgroup.closure k).to_add_group, sub := add_group.sub (add_subgroup.closure k).to_add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul (add_subgroup.closure k).to_add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

source

@[protected]

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

add_subgroup.gi G = {choice := λ (s : set G) (_x : ↑(add_subgroup.closure s) ≤ s), add_subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}

source

@[protected]

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

subgroup.gi G = {choice := λ (s : set G) (_x : ↑(subgroup.closure s) ≤ s), subgroup.closure s, gc := _, le_l_u := _, choice_eq := _}

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.supr_eq_closure {G : Type u_1} [group G] {ι : Sort u_2} (p : ι → subgroup G) :

(⨆ (i : ι), p i) = subgroup.closure (⋃ (i : ι), ↑(p i))

source

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

source

theorem add_subgroup.mem_closure_singleton {G : Type u_1} [add_group G] {x y : G} :

y ∈ add_subgroup.closure {x} ↔ ∃ (n : ℤ), n • x = y

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

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

theorem add_subgroup.closure_singleton_zero {G : Type u_1} [add_group G] :

add_subgroup.closure {0} = ⊥

source

theorem add_subgroup.le_closure_to_add_submonoid {G : Type u_1} [add_group G] (S : set G) :

add_submonoid.closure S ≤ (add_subgroup.closure S).to_add_submonoid

source

theorem subgroup.le_closure_to_submonoid {G : Type u_1} [group G] (S : set G) :

submonoid.closure S ≤ (subgroup.closure S).to_submonoid

source

theorem add_subgroup.closure_eq_top_of_mclosure_eq_top {G : Type u_1} [add_group G] {S : set G} (h : add_submonoid.closure S = ⊤) :

add_subgroup.closure S = ⊤

source

theorem subgroup.closure_eq_top_of_mclosure_eq_top {G : Type u_1} [group G] {S : set G} (h : submonoid.closure S = ⊤) :

subgroup.closure S = ⊤

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 ∈ has_Sup.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 ∈ has_Sup.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

subgroup.comap f H = {carrier := ⇑f ⁻¹' ↑H, mul_mem' := _, one_mem' := _, inv_mem' := _}

Instances for subgroup.comap

subgroup.normal_comap

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

add_subgroup.comap f H = {carrier := ⇑f ⁻¹' ↑H, add_mem' := _, zero_mem' := _, neg_mem' := _}

Instances for add_subgroup.comap

add_subgroup.normal_comap

source

@[simp]

theorem subgroup.coe_comap {G : Type u_1} [group G] {N : Type u_4} [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_4} [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_4} [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_4} [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_4} [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_4} [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_4} [add_group N] {P : Type u_5} [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

mathlib documentation

Subgroups #

Main definitions #

Implementation notes #

Tags #

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

Subgroups #

Main definitions #

Implementation notes #

Tags #

Conversion to/from additive/multiplicative #

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