Subgroups #
This file defines multiplicative and additive subgroups as an extension of submonoids, in a bundled form.
Special thanks goes to Amelia Livingston and Yury Kudryashov for their help and inspiration.
Main definitions #
Notation used here:
G NareGroupsAis anAddGroupH KareSubgroups ofGorAddSubgroups ofAxis an element of typeGor typeAf g : N →* Gare group homomorphismss kare sets of elements of typeG
Definitions in the file:
Subgroup G: the type of subgroups of a groupGAddSubgroup A: the type of subgroups of an additive groupASubgroup.subtype: the natural group homomorphism from a subgroup of groupGtoG
Implementation notes #
Subgroup inclusion is denoted ≤ rather than ⊆, although ∈ is defined as
membership of a subgroup's underlying set.
Tags #
subgroup, subgroups
InvMemClass S G states S is a type of subsets s ⊆ G closed under inverses.
sis closed under inverses
Instances
NegMemClass S G states S is a type of subsets s ⊆ G closed under negation.
sis closed under negation
Instances
Typeclass for substructures s such that s ∪ s⁻¹ = G.
- mem_or_inv_mem (a : G) : a ∈ s ∨ a⁻¹ ∈ s
Instances
theorem
HasMemOrInvMem.inv_mem_of_notMem
{S : Type u_3}
{G : Type u_4}
[Inv G]
[SetLike S G]
(s : S)
[HasMemOrInvMem s]
(x : G)
(h : x ∉ s)
:
x⁻¹ ∈ s
theorem
HasMemOrNegMem.neg_mem_of_notMem
{S : Type u_3}
{G : Type u_4}
[Neg G]
[SetLike S G]
(s : S)
[HasMemOrNegMem s]
(x : G)
(h : x ∉ s)
:
-x ∈ s
theorem
HasMemOrInvMem.mem_of_inv_notMem
{S : Type u_3}
{G : Type u_4}
[Inv G]
[SetLike S G]
(s : S)
[HasMemOrInvMem s]
(x : G)
(h : x⁻¹ ∉ s)
:
x ∈ s
theorem
HasMemOrNegMem.mem_of_neg_notMem
{S : Type u_3}
{G : Type u_4}
[Neg G]
[SetLike S G]
(s : S)
[HasMemOrNegMem s]
(x : G)
(h : -x ∉ s)
:
x ∈ s
class
SubgroupClass
(S : Type u_3)
(G : outParam (Type u_4))
[DivInvMonoid G]
[SetLike S G]
extends SubmonoidClass S G, InvMemClass S G :
SubgroupClass S G states S is a type of subsets s ⊆ G that are subgroups of G.
Instances
class
AddSubgroupClass
(S : Type u_3)
(G : outParam (Type u_4))
[SubNegMonoid G]
[SetLike S G]
extends AddSubmonoidClass S G, NegMemClass S G :
AddSubgroupClass S G states S is a type of subsets s ⊆ G that are
additive subgroups of G.
Instances
@[simp]
theorem
inv_mem_iff
{S : Type u_3}
{G : Type u_4}
[InvolutiveInv G]
{x✝ : SetLike S G}
[InvMemClass S G]
{H : S}
{x : G}
:
x⁻¹ ∈ H ↔ x ∈ H
@[simp]
theorem
neg_mem_iff
{S : Type u_3}
{G : Type u_4}
[InvolutiveNeg G]
{x✝ : SetLike S G}
[NegMemClass S G]
{H : S}
{x : G}
:
-x ∈ H ↔ x ∈ H
theorem
div_mem
{M : Type u_3}
{S : Type u_4}
[DivInvMonoid M]
[SetLike S M]
[hSM : SubgroupClass S M]
{H : S}
{x y : M}
(hx : x ∈ H)
(hy : y ∈ H)
:
x / y ∈ H
A subgroup is closed under division.
theorem
sub_mem
{M : Type u_3}
{S : Type u_4}
[SubNegMonoid M]
[SetLike S M]
[hSM : AddSubgroupClass S M]
{H : S}
{x y : M}
(hx : x ∈ H)
(hy : y ∈ H)
:
x - y ∈ H
An additive subgroup is closed under subtraction.
theorem
zpow_mem
{M : Type u_3}
{S : Type u_4}
[DivInvMonoid M]
[SetLike S M]
[hSM : SubgroupClass S M]
{K : S}
{x : M}
(hx : x ∈ K)
(n : ℤ)
:
x ^ n ∈ K
theorem
zsmul_mem
{M : Type u_3}
{S : Type u_4}
[SubNegMonoid M]
[SetLike S M]
[hSM : AddSubgroupClass S M]
{K : S}
{x : M}
(hx : x ∈ K)
(n : ℤ)
:
n • x ∈ K
theorem
exists_inv_mem_iff_exists_mem
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
{P : G → Prop}
:
(∃ x ∈ H, P x⁻¹) ↔ ∃ x ∈ H, P x
theorem
exists_neg_mem_iff_exists_mem
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
{P : G → Prop}
:
(∃ x ∈ H, P (-x)) ↔ ∃ x ∈ H, P x
theorem
mul_mem_cancel_right
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
{x y : G}
(h : x ∈ H)
:
y * x ∈ H ↔ y ∈ H
theorem
add_mem_cancel_right
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
{x y : G}
(h : x ∈ H)
:
y + x ∈ H ↔ y ∈ H
theorem
mul_mem_cancel_left
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
{x y : G}
(h : x ∈ H)
:
x * y ∈ H ↔ y ∈ H
theorem
add_mem_cancel_left
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
{x y : G}
(h : x ∈ H)
:
x + y ∈ H ↔ y ∈ H
@[implicit_reducible]
instance
InvMemClass.inv
{G : Type u_5}
{S : Type u_6}
[Inv G]
[SetLike S G]
[InvMemClass S G]
{H : S}
:
Inv ↥H
A subgroup of a group inherits an inverse.
@[implicit_reducible]
instance
NegMemClass.neg
{G : Type u_5}
{S : Type u_6}
[Neg G]
[SetLike S G]
[NegMemClass S G]
{H : S}
:
Neg ↥H
An additive subgroup of an AddGroup inherits an inverse.
@[simp]
theorem
InvMemClass.coe_inv
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
(x : ↥H)
:
@[simp]
theorem
NegMemClass.coe_neg
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
(x : ↥H)
:
theorem
SubgroupClass.subset_union
{G : Type u_1}
[Group G]
{S : Type u_4}
[SetLike S G]
[SubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K L : S}
:
theorem
AddSubgroupClass.subset_union
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
[SetLike S G]
[AddSubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K L : S}
:
@[implicit_reducible]
instance
SubgroupClass.div
{G : Type u_5}
{S : Type u_6}
[DivInvMonoid G]
[SetLike S G]
[SubgroupClass S G]
{H : S}
:
Div ↥H
A subgroup of a group inherits a division
@[implicit_reducible]
instance
AddSubgroupClass.sub
{G : Type u_5}
{S : Type u_6}
[SubNegMonoid G]
[SetLike S G]
[AddSubgroupClass S G]
{H : S}
:
Sub ↥H
An additive subgroup of an AddGroup inherits a subtraction.
@[implicit_reducible]
instance
SubgroupClass.instZPow
{M : Type u_5}
{S : Type u_6}
[DivInvMonoid M]
[SetLike S M]
[SubgroupClass S M]
{H : S}
:
Pow ↥H ℤ
A subgroup of a group inherits an integer power.
@[implicit_reducible]
instance
AddSubgroupClass.instZSMul
{M : Type u_5}
{S : Type u_6}
[SubNegMonoid M]
[SetLike S M]
[AddSubgroupClass S M]
{H : S}
:
SMul ℤ ↥H
An additive subgroup of an AddGroup inherits an integer scaling.
@[simp]
theorem
SubgroupClass.coe_div
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
(x y : ↥H)
:
↑(x / y) = ↑x / ↑y
@[simp]
theorem
AddSubgroupClass.coe_sub
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
(x y : ↥H)
:
↑(x - y) = ↑x - ↑y
@[implicit_reducible, instance 75]
instance
SubgroupClass.toGroup
{G : Type u_1}
[Group G]
{S : Type u_4}
(H : S)
[SetLike S G]
[SubgroupClass S G]
:
Group ↥H
A subgroup of a group inherits a group structure.
@[implicit_reducible, instance 75]
instance
AddSubgroupClass.toAddGroup
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
(H : S)
[SetLike S G]
[AddSubgroupClass S G]
:
AddGroup ↥H
An additive subgroup of an AddGroup inherits an AddGroup structure.
@[implicit_reducible, instance 75]
instance
SubgroupClass.toCommGroup
{S : Type u_4}
(H : S)
{G : Type u_5}
[CommGroup G]
[SetLike S G]
[SubgroupClass S G]
:
CommGroup ↥H
@[implicit_reducible, instance 75]
instance
AddSubgroupClass.toAddCommGroup
{S : Type u_4}
(H : S)
{G : Type u_5}
[AddCommGroup G]
[SetLike S G]
[AddSubgroupClass S G]
:
AddCommGroup ↥H
An additive subgroup of an AddCommGroup is an AddCommGroup.
def
SubgroupClass.subtype
{G : Type u_1}
[Group G]
{S : Type u_4}
(H : S)
[SetLike S G]
[SubgroupClass S G]
:
The natural group hom from a subgroup of group G to G.
Instances For
def
AddSubgroupClass.subtype
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
(H : S)
[SetLike S G]
[AddSubgroupClass S G]
:
The natural group hom from an additive subgroup of AddGroup G to G.
Instances For
@[simp]
theorem
SubgroupClass.subtype_apply
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
(x : ↥H)
:
↑H x = ↑x
@[simp]
theorem
AddSubgroupClass.subtype_apply
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
(x : ↥H)
:
↑H x = ↑x
theorem
SubgroupClass.subtype_injective
{G : Type u_1}
[Group G]
{S : Type u_4}
(H : S)
[SetLike S G]
[SubgroupClass S G]
:
Function.Injective ⇑↑H
theorem
AddSubgroupClass.subtype_injective
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
(H : S)
[SetLike S G]
[AddSubgroupClass S G]
:
Function.Injective ⇑↑H
@[simp]
theorem
SubgroupClass.coe_subtype
{G : Type u_1}
[Group G]
{S : Type u_4}
(H : S)
[SetLike S G]
[SubgroupClass S G]
:
⇑↑H = Subtype.val
@[simp]
theorem
AddSubgroupClass.coe_subtype
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
(H : S)
[SetLike S G]
[AddSubgroupClass S G]
:
⇑↑H = Subtype.val
@[simp]
theorem
SubgroupClass.coe_pow
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
(x : ↥H)
(n : ℕ)
:
↑(x ^ n) = ↑x ^ n
@[simp]
theorem
AddSubgroupClass.coe_nsmul
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
(x : ↥H)
(n : ℕ)
:
↑(n • x) = n • ↑x
@[simp]
theorem
SubgroupClass.coe_zpow
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
(x : ↥H)
(n : ℤ)
:
↑(x ^ n) = ↑x ^ n
@[simp]
theorem
AddSubgroupClass.coe_zsmul
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
(x : ↥H)
(n : ℤ)
:
↑(n • x) = n • ↑x
def
SubgroupClass.inclusion
{G : Type u_1}
[Group G]
{S : Type u_4}
[SetLike S G]
[SubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K : S}
(h : H ≤ K)
:
The inclusion homomorphism from a subgroup H contained in K to K.
Instances For
def
AddSubgroupClass.inclusion
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
[SetLike S G]
[AddSubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K : S}
(h : H ≤ K)
:
The inclusion homomorphism from an additive subgroup H contained in K to K.
Instances For
@[simp]
theorem
SubgroupClass.inclusion_self
{G : Type u_1}
[Group G]
{S : Type u_4}
{H : S}
[SetLike S G]
[SubgroupClass S G]
[Preorder S]
[IsConcreteLE S G]
(x : ↥H)
:
(inclusion ⋯) x = x
@[simp]
theorem
AddSubgroupClass.inclusion_self
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H : S}
[SetLike S G]
[AddSubgroupClass S G]
[Preorder S]
[IsConcreteLE S G]
(x : ↥H)
:
(inclusion ⋯) x = x
@[simp]
theorem
SubgroupClass.inclusion_mk
{G : Type u_1}
[Group G]
{S : Type u_4}
{H K : S}
[SetLike S G]
[SubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{h : H ≤ K}
(x : G)
(hx : x ∈ H)
:
(inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
@[simp]
theorem
AddSubgroupClass.inclusion_mk
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H K : S}
[SetLike S G]
[AddSubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{h : H ≤ K}
(x : G)
(hx : x ∈ H)
:
(inclusion h) ⟨x, hx⟩ = ⟨x, ⋯⟩
theorem
SubgroupClass.inclusion_right
{G : Type u_1}
[Group G]
{S : Type u_4}
{H K : S}
[SetLike S G]
[SubgroupClass S G]
[LE S]
[IsConcreteLE S G]
(h : H ≤ K)
(x : ↥K)
(hx : ↑x ∈ H)
:
(inclusion h) ⟨↑x, hx⟩ = x
theorem
AddSubgroupClass.inclusion_right
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
{H K : S}
[SetLike S G]
[AddSubgroupClass S G]
[LE S]
[IsConcreteLE S G]
(h : H ≤ K)
(x : ↥K)
(hx : ↑x ∈ H)
:
(inclusion h) ⟨↑x, hx⟩ = x
@[simp]
theorem
SubgroupClass.inclusion_inclusion
{G : Type u_1}
[Group G]
{S : Type u_4}
{H K : S}
[SetLike S G]
[SubgroupClass S G]
[Preorder S]
[IsConcreteLE S G]
{L : S}
(hHK : H ≤ K)
(hKL : K ≤ L)
(x : ↥H)
:
@[simp]
theorem
SubgroupClass.coe_inclusion
{G : Type u_1}
[Group G]
{S : Type u_4}
[SetLike S G]
[SubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K : S}
(h : H ≤ K)
(a : ↥H)
:
↑((inclusion h) a) = ↑a
@[simp]
theorem
AddSubgroupClass.coe_inclusion
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
[SetLike S G]
[AddSubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K : S}
(h : H ≤ K)
(a : ↥H)
:
↑((inclusion h) a) = ↑a
@[simp]
theorem
SubgroupClass.subtype_comp_inclusion
{G : Type u_1}
[Group G]
{S : Type u_4}
[SetLike S G]
[SubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K : S}
(h : H ≤ K)
:
@[simp]
theorem
AddSubgroupClass.subtype_comp_inclusion
{G : Type u_1}
[AddGroup G]
{S : Type u_4}
[SetLike S G]
[AddSubgroupClass S G]
[LE S]
[IsConcreteLE S G]
{H K : S}
(h : H ≤ K)
:
A subgroup of a group G is a subset containing 1, closed under multiplication
and closed under multiplicative inverse.
Gis closed under inverses
Instances For
An additive subgroup of an additive group G is a subset containing 0, closed
under addition and additive inverse.
Gis closed under negation
Instances For
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
def
Subgroup.ofClass
{S : Type u_3}
{G : Type u_4}
[Group G]
[SetLike S G]
[SubgroupClass S G]
(s : S)
:
Subgroup G
The actual Subgroup obtained from an element of a SubgroupClass
Instances For
def
AddSubgroup.ofClass
{S : Type u_3}
{G : Type u_4}
[AddGroup G]
[SetLike S G]
[AddSubgroupClass S G]
(s : S)
:
The actual AddSubgroup obtained from an element of a
AddSubgroupClass
Instances For
@[simp]
theorem
AddSubgroup.coe_ofClass
{S : Type u_3}
{G : Type u_4}
[AddGroup G]
[SetLike S G]
[AddSubgroupClass S G]
(s : S)
:
↑(ofClass s) = ↑s
@[simp]
theorem
Subgroup.coe_ofClass
{S : Type u_3}
{G : Type u_4}
[Group G]
[SetLike S G]
[SubgroupClass S G]
(s : S)
:
↑(ofClass s) = ↑s
@[instance 100]
instance
Subgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv
{G : Type u_1}
[Group G]
:
@[instance 100]
instance
AddSubgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallNeg
{G : Type u_1}
[AddGroup G]
:
CanLift (Set G) (AddSubgroup G) SetLike.coe fun (s : Set G) =>
0 ∈ s ∧ (∀ {x y : G}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ {x : G}, x ∈ s → -x ∈ s
instance
AddSubgroup.instAddSubgroupClass
{G : Type u_1}
[AddGroup G]
:
AddSubgroupClass (AddSubgroup G) G
theorem
Subgroup.mem_carrier
{G : Type u_1}
[Group G]
{s : Subgroup G}
{x : G}
:
x ∈ s.carrier ↔ x ∈ s
theorem
AddSubgroup.mem_carrier
{G : Type u_1}
[AddGroup G]
{s : AddSubgroup G}
{x : G}
:
x ∈ s.carrier ↔ x ∈ s
@[simp]
theorem
AddSubgroup.mem_mk
{G : Type u_1}
[AddGroup G]
{s : AddSubmonoid G}
{x : G}
(h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier)
:
@[simp]
theorem
AddSubgroup.coe_set_mk
{G : Type u_1}
[AddGroup G]
{s : AddSubmonoid G}
(h_neg : ∀ {x : G}, x ∈ s.carrier → -x ∈ s.carrier)
:
@[simp]
@[simp]
@[simp]
theorem
AddSubgroup.coe_toAddSubmonoid
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
:
↑K.toAddSubmonoid = ↑K
@[simp]
theorem
Subgroup.mem_toSubmonoid
{G : Type u_1}
[Group G]
(K : Subgroup G)
(x : G)
:
x ∈ K.toSubmonoid ↔ x ∈ K
@[simp]
theorem
AddSubgroup.mem_toAddSubmonoid
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
(x : G)
:
x ∈ K.toAddSubmonoid ↔ x ∈ K
theorem
AddSubgroup.toAddSubmonoid_injective
{G : Type u_1}
[AddGroup G]
:
Function.Injective toAddSubmonoid
@[simp]
theorem
Subgroup.toSubmonoid_inj
{G : Type u_1}
[Group G]
{p q : Subgroup G}
:
p.toSubmonoid = q.toSubmonoid ↔ p = q
@[simp]
theorem
AddSubgroup.toAddSubmonoid_inj
{G : Type u_1}
[AddGroup G]
{p q : AddSubgroup G}
:
p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q
@[simp]
theorem
Subgroup.toSubmonoid_le
{G : Type u_1}
[Group G]
{p q : Subgroup G}
:
p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q
@[simp]
theorem
AddSubgroup.toAddSubmonoid_le
{G : Type u_1}
[AddGroup G]
{p q : AddSubgroup G}
:
p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q
@[simp]
@[simp]
Copy of a subgroup with a new carrier equal to the old one. Useful to fix definitional
equalities.
Instances For
Copy of an additive subgroup with a new carrier equal to the old one.
Useful to fix definitional equalities
Instances For
@[simp]
theorem
AddSubgroup.coe_copy
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
(s : Set G)
(hs : s = ↑K)
:
↑(K.copy s hs) = s
@[simp]
theorem
AddSubgroup.copy_eq
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
(s : Set G)
(hs : s = ↑K)
:
K.copy s hs = K
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.
theorem
AddSubgroup.ext
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : ∀ (x : G), x ∈ H ↔ x ∈ K)
:
H = K
Two AddSubgroups are equal if they have the same elements.
theorem
Subgroup.ext_iff
{G : Type u_1}
[Group G]
{H K : Subgroup G}
:
H = K ↔ ∀ (x : G), x ∈ H ↔ x ∈ K
theorem
AddSubgroup.ext_iff
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
:
H = K ↔ ∀ (x : G), x ∈ H ↔ x ∈ K
A subgroup contains the group's 1.
An AddSubgroup contains the group's 0.
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.
theorem
AddSubgroup.add_mem
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
{x y : G}
:
x ∈ H → y ∈ H → x + y ∈ H
An AddSubgroup is closed under addition.
A subgroup is closed under inverse.
An AddSubgroup is closed under inverse.
theorem
Subgroup.div_mem
{G : Type u_1}
[Group G]
(H : Subgroup G)
{x y : G}
(hx : x ∈ H)
(hy : y ∈ H)
:
x / y ∈ H
A subgroup is closed under division.
theorem
AddSubgroup.sub_mem
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
{x y : G}
(hx : x ∈ H)
(hy : y ∈ H)
:
x - y ∈ H
An AddSubgroup is closed under subtraction.
theorem
AddSubgroup.neg_mem_iff
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
{x : G}
:
-x ∈ H ↔ x ∈ H
theorem
AddSubgroup.exists_neg_mem_iff_exists_mem
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
{P : G → Prop}
:
(∃ x ∈ K, P (-x)) ↔ ∃ x ∈ K, P x
theorem
Subgroup.mul_mem_cancel_right
{G : Type u_1}
[Group G]
(H : Subgroup G)
{x y : G}
(h : x ∈ H)
:
y * x ∈ H ↔ y ∈ H
theorem
AddSubgroup.add_mem_cancel_right
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
{x y : G}
(h : x ∈ H)
:
y + x ∈ H ↔ y ∈ H
theorem
Subgroup.mul_mem_cancel_left
{G : Type u_1}
[Group G]
(H : Subgroup G)
{x y : G}
(h : x ∈ H)
:
x * y ∈ H ↔ y ∈ H
theorem
AddSubgroup.add_mem_cancel_left
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
{x y : G}
(h : x ∈ H)
:
x + y ∈ H ↔ y ∈ H
theorem
Subgroup.pow_mem
{G : Type u_1}
[Group G]
(K : Subgroup G)
{x : G}
(hx : x ∈ K)
(n : ℕ)
:
x ^ n ∈ K
theorem
AddSubgroup.nsmul_mem
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
{x : G}
(hx : x ∈ K)
(n : ℕ)
:
n • x ∈ K
theorem
Subgroup.zpow_mem
{G : Type u_1}
[Group G]
(K : Subgroup G)
{x : G}
(hx : x ∈ K)
(n : ℤ)
:
x ^ n ∈ K
theorem
AddSubgroup.zsmul_mem
{G : Type u_1}
[AddGroup G]
(K : AddSubgroup G)
{x : G}
(hx : x ∈ K)
(n : ℤ)
:
n • x ∈ K
@[implicit_reducible]
A subgroup of a group inherits a multiplication.
@[implicit_reducible]
An AddSubgroup of an AddGroup inherits an addition.
@[implicit_reducible]
A subgroup of a group inherits a 1.
@[implicit_reducible]
An AddSubgroup of an AddGroup inherits a zero.
@[implicit_reducible]
A subgroup of a group inherits an inverse.
@[implicit_reducible]
An AddSubgroup of an AddGroup inherits an inverse.
@[implicit_reducible]
A subgroup of a group inherits a division
@[implicit_reducible]
An AddSubgroup of an AddGroup inherits a subtraction.
@[implicit_reducible]
A subgroup of a group inherits a natural power
@[implicit_reducible]
An AddSubgroup of an AddGroup inherits a natural scaling.
@[implicit_reducible]
A subgroup of a group inherits an integer power
@[implicit_reducible]
An AddSubgroup of an AddGroup inherits an integer scaling.
@[simp]
@[simp]
theorem
AddSubgroup.coe_add
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
(x y : ↥H)
:
↑(x + y) = ↑x + ↑y
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
AddSubgroup.coe_sub
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
(x y : ↥H)
:
↑(x - y) = ↑x - ↑y
theorem
Subgroup.coe_mk
{G : Type u_1}
[Group G]
(H : Subgroup G)
(x : G)
(hx : x ∈ H)
:
↑⟨x, hx⟩ = x
theorem
AddSubgroup.coe_mk
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
(x : G)
(hx : x ∈ H)
:
↑⟨x, hx⟩ = x
@[simp]
theorem
Subgroup.coe_pow
{G : Type u_1}
[Group G]
(H : Subgroup G)
(x : ↥H)
(n : ℕ)
:
↑(x ^ n) = ↑x ^ n
@[simp]
theorem
AddSubgroup.coe_nsmul
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
(x : ↥H)
(n : ℕ)
:
↑(n • x) = n • ↑x
theorem
Subgroup.coe_zpow
{G : Type u_1}
[Group G]
(H : Subgroup G)
(x : ↥H)
(n : ℤ)
:
↑(x ^ n) = ↑x ^ n
theorem
AddSubgroup.coe_zsmul
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
(x : ↥H)
(n : ℤ)
:
↑(n • x) = n • ↑x
@[simp]
theorem
Subgroup.mk_eq_one
{G : Type u_1}
[Group G]
(H : Subgroup G)
{g : G}
{h : g ∈ H}
:
⟨g, h⟩ = 1 ↔ g = 1
@[simp]
theorem
AddSubgroup.mk_eq_zero
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
{g : G}
{h : g ∈ H}
:
⟨g, h⟩ = 0 ↔ g = 0
@[implicit_reducible]
A subgroup of a group inherits a group structure.
@[implicit_reducible]
An AddSubgroup of an AddGroup inherits an AddGroup structure.
@[implicit_reducible]
@[implicit_reducible]
instance
AddSubgroup.toAddCommGroup
{G : Type u_3}
[AddCommGroup G]
(H : AddSubgroup G)
:
AddCommGroup ↥H
An AddSubgroup of an AddCommGroup is an AddCommGroup.
The natural group hom from a subgroup of group G to G.
Instances For
The natural group hom from an AddSubgroup of AddGroup G to G.
Instances For
@[simp]
@[simp]
theorem
AddSubgroup.subtype_apply
{G : Type u_1}
[AddGroup G]
{s : AddSubgroup G}
(x : ↥s)
:
s.subtype x = ↑x
theorem
Subgroup.subtype_injective
{G : Type u_1}
[Group G]
(s : Subgroup G)
:
Function.Injective ⇑s.subtype
theorem
AddSubgroup.subtype_injective
{G : Type u_1}
[AddGroup G]
(s : AddSubgroup G)
:
Function.Injective ⇑s.subtype
@[simp]
@[simp]
theorem
AddSubgroup.coe_subtype
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
:
⇑H.subtype = Subtype.val
The inclusion homomorphism from a subgroup H contained in K to K.
Instances For
The inclusion homomorphism from an additive subgroup H contained in K to K.
Instances For
@[simp]
@[simp]
theorem
AddSubgroup.coe_inclusion
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H ≤ K)
(a : ↥H)
:
↑((inclusion h) a) = ↑a
theorem
AddSubgroup.inclusion_injective
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H ≤ K)
:
Function.Injective ⇑(inclusion h)
@[simp]
@[simp]
theorem
AddSubgroup.inclusion_inj
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(h : H ≤ K)
{x y : ↥H}
:
@[simp]
theorem
AddSubgroup.subtype_comp_inclusion
{G : Type u_1}
[AddGroup G]
{H K : AddSubgroup G}
(hH : H ≤ K)
:
A subgroup H is normal if whenever n ∈ H, then g * n * g⁻¹ ∈ H for every g : G
- conj_mem (n : G) : n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H
His closed under conjugation
Instances
An AddSubgroup H is normal if whenever n ∈ H, then g + n - g ∈ H for every g : A
- conj_mem (n : A) : n ∈ H → ∀ (g : A), g + n + -g ∈ H
His closed under additive conjugation
Instances
@[instance 100]
@[instance 100]
theorem
AddSubgroup.Normal.addConj_mem'
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
(nH : H.Normal)
(n : G)
(hn : n ∈ H)
(g : G)
:
-g + n + g ∈ H
theorem
Subgroup.Normal.mem_comm
{G : Type u_1}
[Group G]
{H : Subgroup G}
(nH : H.Normal)
{a b : G}
(h : a * b ∈ H)
:
b * a ∈ H
theorem
AddSubgroup.Normal.mem_comm
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
(nH : H.Normal)
{a b : G}
(h : a + b ∈ H)
:
b + a ∈ H
theorem
Subgroup.Normal.mem_comm_iff
{G : Type u_1}
[Group G]
{H : Subgroup G}
(nH : H.Normal)
{a b : G}
:
a * b ∈ H ↔ b * a ∈ H
theorem
AddSubgroup.Normal.mem_comm_iff
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
(nH : H.Normal)
{a b : G}
:
a + b ∈ H ↔ b + a ∈ H
The normalizer of S is the subgroup of G whose elements satisfy g * S * g⁻¹ = S.
When S is a subgroup, this is the largest subgroup of G inside which S is normal.
Instances For
The normalizer of S is the subgroup of G whose elements satisfy g + S - g = S.
When S is a subgroup, this is the largest subgroup of G inside which S is normal.
Instances For
@[deprecated Subgroup.normalizer (since := "2026-03-19")]
Alias of Subgroup.normalizer.
The normalizer of S is the subgroup of G whose elements satisfy g * S * g⁻¹ = S.
When S is a subgroup, this is the largest subgroup of G inside which S is normal.
Instances For
theorem
Subgroup.mem_normalizer_iff
{G : Type u_1}
[Group G]
{H : Subgroup G}
{g : G}
:
g ∈ normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ g * h * g⁻¹ ∈ H
theorem
AddSubgroup.mem_normalizer_iff
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
{g : G}
:
g ∈ normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ g + h + -g ∈ H
theorem
Subgroup.mem_normalizer_iff''
{G : Type u_1}
[Group G]
{H : Subgroup G}
{g : G}
:
g ∈ normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ g⁻¹ * h * g ∈ H
theorem
AddSubgroup.mem_normalizer_iff''
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
{g : G}
:
g ∈ normalizer ↑H ↔ ∀ (h : G), h ∈ H ↔ -g + h + g ∈ H
theorem
Subgroup.mem_normalizer_iff'
{G : Type u_1}
[Group G]
{H : Subgroup G}
{g : G}
:
g ∈ normalizer ↑H ↔ ∀ (n : G), n * g ∈ H ↔ g * n ∈ H
theorem
AddSubgroup.mem_normalizer_iff'
{G : Type u_1}
[AddGroup G]
{H : AddSubgroup G}
{g : G}
:
g ∈ normalizer ↑H ↔ ∀ (n : G), n + g ∈ H ↔ g + n ∈ H
A subgroup of a commutative group is commutative.
instance
AddSubgroup.addCommGroup_isAddCommutative
{G : Type u_3}
[AddCommGroup G]
(H : AddSubgroup G)
:
A subgroup of a commutative group is commutative.
@[deprecated setLike_mul_comm (since := "2026-03-09")]
theorem
Subgroup.mul_comm_of_mem_isMulCommutative
{G : Type u_1}
[Group G]
(H : Subgroup G)
[IsMulCommutative ↥H]
{a b : G}
(ha : a ∈ H)
(hb : b ∈ H)
:
a * b = b * a
@[deprecated setLike_mul_comm (since := "2026-03-09")]
theorem
AddSubgroup.add_comm_of_mem_isAddCommutative
{G : Type u_1}
[AddGroup G]
(H : AddSubgroup G)
[IsAddCommutative ↥H]
{a b : G}
(ha : a ∈ H)
(hb : b ∈ H)
:
a + b = b + a
theorem
Set.injOn_iff_map_eq_one
{F : Type u_3}
{G : Type u_4}
{H : Type u_5}
{S : Type u_6}
[Group G]
[Group H]
[FunLike F G H]
[MonoidHomClass F G H]
(f : F)
[SetLike S G]
[OneMemClass S G]
[MulMemClass S G]
[InvMemClass S G]
(s : S)
:
InjOn ⇑f ↑s ↔ ∀ a ∈ s, f a = 1 → a = 1
theorem
Set.injOn_iff_map_eq_zero
{F : Type u_3}
{G : Type u_4}
{H : Type u_5}
{S : Type u_6}
[AddGroup G]
[AddGroup H]
[FunLike F G H]
[AddMonoidHomClass F G H]
(f : F)
[SetLike S G]
[ZeroMemClass S G]
[AddMemClass S G]
[NegMemClass S G]
(s : S)
:
InjOn ⇑f ↑s ↔ ∀ a ∈ s, f a = 0 → a = 0