doc-next-gen

Mathlib.Algebra.Group.Subgroup.Defs

Module docstring

{"# Subgroups

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

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

Main definitions

Notation used here:

  • G N are Groups

  • A is an AddGroup

  • H K are Subgroups of G or AddSubgroups of A

  • x is an element of type G or type A

  • f g : N →* G are group homomorphisms

  • s k are sets of elements of type G

Definitions in the file:

  • Subgroup G : the type of subgroups of a group G

  • AddSubgroup A : the type of subgroups of an additive group A

  • Subgroup.subtype : the natural group homomorphism from a subgroup of group G to G

Implementation notes

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

Tags

subgroup, subgroups "}

InvMemClass structure
(S : Type*) (G : outParam Type*) [Inv G] [SetLike S G]
Full source 
/-- `InvMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/
class InvMemClass (S : Type*) (G : outParam Type*) [Inv G] [SetLike S G] : Prop where
  /-- `s` is closed under inverses -/
  inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹x⁻¹ ∈ s
Subsets Closed Under Inversion
Informal description
The structure `InvMemClass S G` states that a type `S` represents subsets of a type `G` equipped with an inversion operation, and these subsets are closed under inversion. That is, for any subset `s : S` and any element `x ∈ s`, the inverse `x⁻¹` is also in `s`.
NegMemClass structure
(S : Type*) (G : outParam Type*) [Neg G] [SetLike S G]
Full source 
/-- `NegMemClass S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
class NegMemClass (S : Type*) (G : outParam Type*) [Neg G] [SetLike S G] : Prop where
  /-- `s` is closed under negation -/
  neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s
Subsets Closed under Negation
Informal description
The structure `NegMemClass S G` states that for a type `S` representing subsets of a type `G` equipped with a negation operation, every subset `s : S` is closed under negation. That is, if an element `x` belongs to `s`, then its negation `-x` also belongs to `s`.
SubgroupClass structure
(S : Type*) (G : outParam Type*) [DivInvMonoid G] [SetLike S G] : Prop extends SubmonoidClass S G, InvMemClass S G
Full source 
/-- `SubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
class SubgroupClass (S : Type*) (G : outParam Type*) [DivInvMonoid G] [SetLike S G] : Prop
    extends SubmonoidClass S G, InvMemClass S G
Subgroup Class
Informal description
A type `S` is a `SubgroupClass` of a group `G` if it represents a collection of subsets of `G` that are closed under the group operations (multiplication, inversion, and contains the identity element). This means any subset `H` of type `S` is a subgroup of `G`. More formally, for a type `G` equipped with a division-inversion monoid structure and a type `S` with a `SetLike` instance for `G`, `SubgroupClass S G` asserts that every term of type `S` is a subgroup of `G`. This extends the properties of `SubmonoidClass` (closure under multiplication and containing the identity) with the additional requirement of closure under inversion.
AddSubgroupClass structure
(S : Type*) (G : outParam Type*) [SubNegMonoid G] [SetLike S G] : Prop extends AddSubmonoidClass S G, NegMemClass S G
Full source 
/-- `AddSubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are
additive subgroups of `G`. -/
class AddSubgroupClass (S : Type*) (G : outParam Type*) [SubNegMonoid G] [SetLike S G] : Prop
    extends AddSubmonoidClass S G, NegMemClass S G
Additive Subgroup Class
Informal description
The structure `AddSubgroupClass S G` asserts that `S` is a type of subsets of an additive group `G` that are closed under the group operations. Specifically, it extends `AddSubmonoidClass` (ensuring closure under addition and containing the zero element) and `NegMemClass` (ensuring closure under negation). More formally, for a type `S` to be an `AddSubgroupClass` of `G`, the following must hold: 1. The elements of `S` are subsets of `G` (via `SetLike`). 2. The subsets in `S` are additive submonoids of `G` (i.e., closed under addition and contain `0`). 3. The subsets in `S` are closed under negation (i.e., if `x` is in a subset, then `-x` is also in the subset). This structure is used to define additive subgroups in a bundled form, where the subset itself is equipped with the structure of an additive group.
inv_mem_iff theorem
{S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S} {x : G} : x⁻¹ ∈ H ↔ x ∈ H
Full source 
@[to_additive (attr := simp)]
theorem inv_mem_iff {S G} [InvolutiveInv G] {_ : SetLike S G} [InvMemClass S G] {H : S}
    {x : G} : x⁻¹x⁻¹ ∈ Hx⁻¹ ∈ H ↔ x ∈ H :=
  ⟨fun h => inv_inv x ▸ inv_mem h, inv_mem⟩
Inversion Membership Criterion: $x^{-1} \in H \leftrightarrow x \in H$
Informal description
Let $G$ be a group with an involutive inversion operation, and let $S$ be a set-like structure for $G$ that is closed under inversion. For any subset $H$ of $G$ (represented by an element of $S$) and any element $x \in G$, the inverse $x^{-1}$ belongs to $H$ if and only if $x$ belongs to $H$.
div_mem theorem
{x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H
Full source 
/-- A subgroup is closed under division. -/
@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))
  "An additive subgroup is closed under subtraction."]
theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H := by
  rw [div_eq_mul_inv]; exact mul_mem hx (inv_mem hy)
Closure of Subgroup under Division
Informal description
Let $H$ be a subgroup of a group $G$. For any elements $x, y \in G$ such that $x \in H$ and $y \in H$, the quotient $x / y$ is also in $H$.
zpow_mem theorem
{x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
Full source 
@[to_additive (attr := aesop safe apply (rule_sets := [SetLike]))]
theorem zpow_mem {x : M} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
  | (n : ℕ) => by
    rw [zpow_natCast]
    exact pow_mem hx n
  | -[n+1] => by
    rw [zpow_negSucc]
    exact inv_mem (pow_mem hx n.succ)
Closure of Subgroups under Integer Powers: $x \in K \Rightarrow x^n \in K$ for all $n \in \mathbb{Z}$
Informal description
Let $G$ be a group and $K$ a subgroup of $G$. For any element $x \in K$ and any integer $n$, the power $x^n$ belongs to $K$.
exists_inv_mem_iff_exists_mem theorem
{P : G → Prop} : (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x
Full source 
@[to_additive]
theorem exists_inv_mem_iff_exists_mem {P : G → Prop} :
    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x := by
  constructor <;>
    · rintro ⟨x, x_in, hx⟩
      exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩
Existence of Inverse in Subgroup iff Existence of Element Satisfying Predicate
Informal description
For any subgroup $H$ of a group $G$ and any predicate $P$ on $G$, there exists an element $x \in G$ such that $x \in H$ and $P(x^{-1})$ holds if and only if there exists an element $x \in H$ such that $P(x)$ holds.
mul_mem_cancel_right theorem
{x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H
Full source 
@[to_additive]
theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ Hy * x ∈ H ↔ y ∈ H :=
  ⟨fun hba => by simpa using mul_mem hba (inv_mem h), fun hb => mul_mem hb h⟩
Right Multiplication Cancellation in Subgroups: $y \cdot x \in H \leftrightarrow y \in H$ for $x \in H$
Informal description
Let $H$ be a subgroup of a group $G$. For any elements $x, y \in G$ such that $x \in H$, we have $y \cdot x \in H$ if and only if $y \in H$.
mul_mem_cancel_left theorem
{x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H
Full source 
@[to_additive]
theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ Hx * y ∈ H ↔ y ∈ H :=
  ⟨fun hab => by simpa using mul_mem (inv_mem h) hab, mul_mem h⟩
Left Multiplication Cancellation in Subgroups: $x \cdot y \in H \leftrightarrow y \in H$ for $x \in H$
Informal description
Let $H$ be a subgroup of a group $G$. For any elements $x, y \in G$ such that $x \in H$, we have $x \cdot y \in H$ if and only if $y \in H$.
InvMemClass.inv instance
{G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G] [InvMemClass S G] {H : S} : Inv H
Full source 
/-- A subgroup of a group inherits an inverse. -/
@[to_additive "An additive subgroup of an `AddGroup` inherits an inverse."]
instance inv {G : Type u_1} {S : Type u_2} [Inv G] [SetLike S G]
  [InvMemClass S G] {H : S} : Inv H :=
  ⟨fun a => ⟨a⁻¹, inv_mem a.2⟩⟩
Inversion Operation on Subgroups Closed Under Inversion
Informal description
For any subset $H$ of a group $G$ that is closed under inversion (i.e., $x \in H$ implies $x^{-1} \in H$), $H$ inherits an inversion operation from $G$.
InvMemClass.coe_inv theorem
(x : H) : (x⁻¹).1 = x.1⁻¹
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_inv (x : H) : (x⁻¹).1 = x.1⁻¹ :=
  rfl
Inversion Commutes with Subgroup Coercion: $(x^{-1})_1 = (x_1)^{-1}$
Informal description
For any element $x$ in a subgroup $H$ of a group $G$, the first projection of the inverse of $x$ in $H$ is equal to the inverse of the first projection of $x$ in $G$. In other words, if we consider $x$ as an element of $G$ via the coercion, then $(x^{-1})_1 = (x_1)^{-1}$.
SubgroupClass.subset_union theorem
{H K L : S} : (H : Set G) ⊆ K ∪ L ↔ H ≤ K ∨ H ≤ L
Full source 
@[to_additive]
theorem subset_union {H K L : S} : (H : Set G) ⊆ K ∪ L(H : Set G) ⊆ K ∪ L ↔ H ≤ K ∨ H ≤ L := by
  refine ⟨fun h ↦ ?_, fun h x xH ↦ h.imp (· xH) (· xH)⟩
  rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
  exact fun ⟨x, xH, xK⟩ y yH ↦ (h <| mul_mem xH yH).elim
    ((h yH).resolve_left fun yK ↦ xK <| (mul_mem_cancel_right yK).mp ·)
    (mul_mem_cancel_left <| (h xH).resolve_left xK).mp
Subgroup Inclusion in Union of Subgroups: $H \subseteq K \cup L \leftrightarrow H \leq K \lor H \leq L$
Informal description
Let $G$ be a group and $H, K, L$ be subgroups of $G$ (represented as elements of type $S$ where $S$ is a `SubgroupClass` of $G$). Then the subset inclusion $H \subseteq K \cup L$ holds if and only if either $H$ is a subgroup of $K$ or $H$ is a subgroup of $L$.
SubgroupClass.div instance
{G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G] [SubgroupClass S G] {H : S} : Div H
Full source 
/-- A subgroup of a group inherits a division -/
@[to_additive "An additive subgroup of an `AddGroup` inherits a subtraction."]
instance div {G : Type u_1} {S : Type u_2} [DivInvMonoid G] [SetLike S G]
  [SubgroupClass S G] {H : S} : Div H :=
  ⟨fun a b => ⟨a / b, div_mem a.2 b.2⟩⟩
Division Operation Inherited by Subgroups
Informal description
For any subgroup $H$ of a group $G$ equipped with a division-inversion monoid structure, $H$ inherits a division operation from $G$.
AddSubgroupClass.zsmul instance
{M S} [SubNegMonoid M] [SetLike S M] [AddSubgroupClass S M] {H : S} : SMul ℤ H
Full source 
/-- An additive subgroup of an `AddGroup` inherits an integer scaling. -/
instance _root_.AddSubgroupClass.zsmul {M S} [SubNegMonoid M] [SetLike S M]
    [AddSubgroupClass S M] {H : S} : SMul ℤ H :=
  ⟨fun n a => ⟨n • a.1, zsmul_mem a.2 n⟩⟩
Integer Scalar Multiplication on Additive Subgroups
Informal description
For any additive subgroup $H$ of an additive group $M$ (where $M$ is a subtraction-negation monoid), $H$ inherits an integer scalar multiplication operation from $M$.
SubgroupClass.zpow instance
{M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ
Full source 
/-- A subgroup of a group inherits an integer power. -/
@[to_additive existing]
instance zpow {M S} [DivInvMonoid M] [SetLike S M] [SubgroupClass S M] {H : S} : Pow H ℤ :=
  ⟨fun a n => ⟨a.1 ^ n, zpow_mem a.2 n⟩⟩
Integer Powers in Subgroups
Informal description
For any subgroup $H$ of a group $G$ equipped with a division-inversion monoid structure, $H$ inherits an integer power operation from $G$. Specifically, for any $h \in H$ and $n \in \mathbb{Z}$, the element $h^n$ is well-defined and remains in $H$.
SubgroupClass.coe_div theorem
(x y : H) : (x / y).1 = x.1 / y.1
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_div (x y : H) : (x / y).1 = x.1 / y.1 :=
  rfl
Subgroup Division Coercion: $(x / y).1 = x.1 / y.1$
Informal description
For any subgroup $H$ of a group $G$ and any elements $x, y \in H$, the first projection (i.e., the underlying element in $G$) of the quotient $x / y$ in $H$ is equal to the quotient of the underlying elements $x.1 / y.1$ in $G$.
SubgroupClass.toGroup instance
: Group H
Full source 
/-- A subgroup of a group inherits a group structure. -/
@[to_additive "An additive subgroup of an `AddGroup` inherits an `AddGroup` structure."]
instance (priority := 75) toGroup : Group H := fast_instance%
  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Subgroup Inherits Group Structure
Informal description
For any subgroup $H$ of a group $G$, $H$ inherits a group structure from $G$. This means $H$ is equipped with a multiplication operation, an identity element, and an inversion operation, satisfying the group axioms.
SubgroupClass.toCommGroup instance
{G : Type*} [CommGroup G] [SetLike S G] [SubgroupClass S G] : CommGroup H
Full source 
/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
@[to_additive "An additive subgroup of an `AddCommGroup` is an `AddCommGroup`."]
instance (priority := 75) toCommGroup {G : Type*} [CommGroup G] [SetLike S G] [SubgroupClass S G] :
    CommGroup H := fast_instance%
  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Subgroups of Commutative Groups are Commutative
Informal description
For any commutative group $G$ and any subgroup $H$ of $G$, $H$ inherits a commutative group structure from $G$.
SubgroupClass.subtype definition
: H →* G
Full source 
/-- The natural group hom from a subgroup of group `G` to `G`. -/
@[to_additive (attr := coe)
  "The natural group hom from an additive subgroup of `AddGroup` `G` to `G`."]
protected def subtype : H →* G where
  toFun := ((↑) : H → G); map_one' := rfl; map_mul' := fun _ _ => rfl
Subgroup inclusion homomorphism
Informal description
The natural group homomorphism from a subgroup \( H \) of a group \( G \) to \( G \) itself, defined by the inclusion map \( x \mapsto x \). This homomorphism preserves the group structure, i.e., it maps the identity to the identity and the product of two elements to their product in \( G \).
SubgroupClass.subtype_apply theorem
(x : H) : SubgroupClass.subtype H x = x
Full source 
@[to_additive (attr := simp)]
lemma subtype_apply (x : H) :
    SubgroupClass.subtype H x = x := rfl
Subgroup Inclusion Homomorphism Acts as Identity on Elements
Informal description
For any element $x$ in a subgroup $H$ of a group $G$, the natural inclusion homomorphism $\text{subtype} \colon H \to G$ maps $x$ to itself, i.e., $\text{subtype}(x) = x$.
SubgroupClass.subtype_injective theorem
: Function.Injective (SubgroupClass.subtype H)
Full source 
@[to_additive]
lemma subtype_injective :
    Function.Injective (SubgroupClass.subtype H) :=
  Subtype.coe_injective
Injectivity of Subgroup Inclusion Homomorphism
Informal description
The inclusion homomorphism from a subgroup $H$ of a group $G$ to $G$ is injective. That is, if two elements of $H$ have the same image in $G$ under the inclusion map, then they are equal in $H$.
SubgroupClass.coe_subtype theorem
: (SubgroupClass.subtype H : H → G) = ((↑) : H → G)
Full source 
@[to_additive (attr := simp)]
theorem coe_subtype : (SubgroupClass.subtype H : H → G) = ((↑) : H → G) := by
  rfl
Subgroup Inclusion Homomorphism Equals Coercion
Informal description
The group homomorphism `SubgroupClass.subtype H` from a subgroup $H$ of a group $G$ to $G$ itself is equal to the coercion function $(↑) \colon H \to G$.
SubgroupClass.coe_pow theorem
(x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
  rfl
Subgroup Power Operation Agrees with Group Power Operation
Informal description
For any subgroup $H$ of a group $G$ and any element $x \in H$, the $n$-th power of $x$ in $H$ (denoted $(x^n : H)$) is equal to the $n$-th power of $x$ in $G$ (denoted $x^n$). In other words, the power operation in the subgroup agrees with the power operation in the ambient group.
SubgroupClass.coe_zpow theorem
(x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n :=
  rfl
Subgroup Integer Power Operation Agrees with Group Integer Power Operation
Informal description
For any subgroup $H$ of a group $G$ and any element $x \in H$, the $n$-th integer power of $x$ in $H$ (denoted $(x^n : H)$) is equal to the $n$-th integer power of $x$ in $G$ (denoted $x^n$). In other words, the integer power operation in the subgroup agrees with the integer power operation in the ambient group.
SubgroupClass.inclusion definition
{H K : S} (h : H ≤ K) : H →* K
Full source 
/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
def inclusion {H K : S} (h : H ≤ K) : H →* K :=
  MonoidHom.mk' (fun x => ⟨x, h x.prop⟩) fun _ _=> rfl
Inclusion homomorphism between subgroups
Informal description
Given two subgroups \( H \) and \( K \) of a group \( G \) such that \( H \) is contained in \( K \) (denoted \( H \leq K \)), the inclusion homomorphism is the group homomorphism that maps each element \( x \in H \) to itself considered as an element of \( K \).
SubgroupClass.inclusion_self theorem
(x : H) : inclusion le_rfl x = x
Full source 
@[to_additive (attr := simp)]
theorem inclusion_self (x : H) : inclusion le_rfl x = x := by
  cases x
  rfl
Inclusion Homomorphism is Identity on Subgroup Elements
Informal description
For any element $x$ in a subgroup $H$ of a group $G$, the inclusion homomorphism from $H$ to itself (induced by the reflexive relation $H \leq H$) maps $x$ to itself, i.e., $\text{inclusion}(\text{le\_rfl})(x) = x$.
SubgroupClass.inclusion_mk theorem
{h : H ≤ K} (x : G) (hx : x ∈ H) : inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩
Full source 
@[to_additive (attr := simp)]
theorem inclusion_mk {h : H ≤ K} (x : G) (hx : x ∈ H) : inclusion h ⟨x, hx⟩ = ⟨x, h hx⟩ :=
  rfl
Inclusion Homomorphism Maps Elements Preserving Membership Proofs
Informal description
Let $G$ be a group and let $H, K$ be subgroups of $G$ such that $H \leq K$. For any element $x \in G$ that belongs to $H$, the inclusion homomorphism maps the element $\langle x, hx \rangle$ of $H$ to $\langle x, h hx \rangle$ in $K$, where $hx$ is the proof that $x \in H$ and $h hx$ is the proof that $x \in K$ obtained from the inclusion $H \leq K$.
SubgroupClass.inclusion_right theorem
(h : H ≤ K) (x : K) (hx : (x : G) ∈ H) : inclusion h ⟨x, hx⟩ = x
Full source 
@[to_additive]
theorem inclusion_right (h : H ≤ K) (x : K) (hx : (x : G) ∈ H) : inclusion h ⟨x, hx⟩ = x := by
  cases x
  rfl
Right Inclusion of Subgroup Elements Preserves Identity
Informal description
Let $G$ be a group and let $H$ and $K$ be subgroups of $G$ such that $H \leq K$. For any element $x \in K$ that also belongs to $H$, the inclusion homomorphism from $H$ to $K$ maps the element $\langle x, hx \rangle$ (where $hx$ is the proof that $x \in H$) to $x$ itself.
SubgroupClass.inclusion_inclusion theorem
{L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) : inclusion hKL (inclusion hHK x) = inclusion (hHK.trans hKL) x
Full source 
@[simp]
theorem inclusion_inclusion {L : S} (hHK : H ≤ K) (hKL : K ≤ L) (x : H) :
    inclusion hKL (inclusion hHK x) = inclusion (hHK.trans hKL) x := by
  cases x
  rfl
Composition of Subgroup Inclusion Homomorphisms
Informal description
Let $G$ be a group and let $H$, $K$, and $L$ be subgroups of $G$ such that $H \leq K \leq L$. For any element $x \in H$, the composition of the inclusion homomorphisms $H \hookrightarrow K$ and $K \hookrightarrow L$ applied to $x$ equals the inclusion homomorphism $H \hookrightarrow L$ applied to $x$. In other words, if $h_{HK} \colon H \leq K$ and $h_{KL} \colon K \leq L$ are the subgroup inclusions, then for any $x \in H$, \[ h_{KL}(h_{HK}(x)) = (h_{HK} \circ h_{KL})(x). \]
SubgroupClass.coe_inclusion theorem
{H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a
Full source 
@[to_additive (attr := simp)]
theorem coe_inclusion {H K : S} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
  cases a
  simp only [inclusion, MonoidHom.mk'_apply]
Inclusion Homomorphism Preserves Elements in Subgroups
Informal description
Let $G$ be a group and let $H$ and $K$ be subgroups of $G$ such that $H \leq K$. For any element $a \in H$, the image of $a$ under the inclusion homomorphism from $H$ to $K$ (considered as an element of $G$) is equal to $a$ itself. In other words, the inclusion homomorphism preserves the underlying elements of $G$.
SubgroupClass.subtype_comp_inclusion theorem
{H K : S} (hH : H ≤ K) : (SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H
Full source 
@[to_additive (attr := simp)]
theorem subtype_comp_inclusion {H K : S} (hH : H ≤ K) :
    (SubgroupClass.subtype K).comp (inclusion hH) = SubgroupClass.subtype H := by
  ext
  simp only [MonoidHom.comp_apply, coe_subtype, coe_inclusion]
Compatibility of Subgroup Inclusions with Composition
Informal description
Let $G$ be a group and let $H$ and $K$ be subgroups of $G$ such that $H \leq K$. The composition of the inclusion homomorphism $H \hookrightarrow K$ with the subgroup inclusion homomorphism $K \hookrightarrow G$ equals the subgroup inclusion homomorphism $H \hookrightarrow G$. In other words, the following diagram commutes: \[ \begin{CD} H @>{inclusion\ hH}>> K \\ @V{subtype\ H}VV @VV{subtype\ K}V \\ G @= G \end{CD} \]
Subgroup structure
(G : Type*) [Group G] extends Submonoid G
Full source 
/-- A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse. -/
structure Subgroup (G : Type*) [Group G] extends Submonoid G where
  /-- `G` is closed under inverses -/
  inv_mem' {x} : x ∈ carrier → x⁻¹x⁻¹ ∈ carrier
Subgroup of a group
Informal description
A subgroup of a group $G$ is a subset of $G$ that contains the identity element, is closed under the group operation (multiplication), and is closed under taking inverses.
AddSubgroup structure
(G : Type*) [AddGroup G] extends AddSubmonoid G
Full source 
/-- An additive subgroup of an additive group `G` is a subset containing 0, closed
under addition and additive inverse. -/
structure AddSubgroup (G : Type*) [AddGroup G] extends AddSubmonoid G where
  /-- `G` is closed under negation -/
  neg_mem' {x} : x ∈ carrier → -x ∈ carrier
Additive Subgroup
Informal description
An additive subgroup of an additive group $G$ is a subset of $G$ containing the additive identity $0$, closed under addition and additive inverses.
Subgroup.instSetLike instance
: SetLike (Subgroup G) G
Full source 
@[to_additive]
instance : SetLike (Subgroup G) G where
  coe s := s.carrier
  coe_injective' p q h := by
    obtain ⟨⟨⟨hp,_⟩,_⟩,_⟩ := p
    obtain ⟨⟨⟨hq,_⟩,_⟩,_⟩ := q
    congr
Set-like Structure for Subgroups
Informal description
For any group $G$, the type of subgroups of $G$ can be treated as a set-like structure, where each subgroup is naturally associated with its underlying subset of $G$. This means that subgroup inclusion can be checked via set membership, and two subgroups are equal if and only if they contain the same elements of $G$.
Subgroup.ofClass definition
{S G : Type*} [Group G] [SetLike S G] [SubgroupClass S G] (s : S) : Subgroup G
Full source 
/-- The actual `Subgroup` obtained from an element of a `SubgroupClass` -/
@[to_additive (attr := simps) "The actual `AddSubgroup` obtained from an element of a
`AddSubgroupClass`"]
def ofClass {S G : Type*} [Group G] [SetLike S G] [SubgroupClass S G]
    (s : S) : Subgroup G :=
  ⟨⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩, InvMemClass.inv_mem⟩
Subgroup construction from a subgroup class element
Informal description
Given a type `S` with a `SetLike` instance for a group `G` and a `SubgroupClass` instance for `S`, the function `Subgroup.ofClass` constructs a subgroup of `G` from an element `s : S`. The resulting subgroup has the same carrier set as `s` and inherits the closure properties under multiplication, identity, and inverses from the `SubgroupClass` structure.
Subgroup.instCanLiftSetCoeAndMemOfNatForallForallForallForallHMulForallForallInv instance
: CanLift (Set G) (Subgroup G) (↑) (fun s ↦ 1 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → x⁻¹ ∈ s)
Full source 
@[to_additive]
instance (priority := 100) : CanLift (Set G) (Subgroup G) (↑)
    (fun s ↦ 1 ∈ s1 ∈ s ∧ (∀ {x y}, x ∈ s → y ∈ s → x * y ∈ s) ∧ ∀ {x}, x ∈ s → x⁻¹ ∈ s) where
  prf s h := ⟨{ carrier := s, one_mem' := h.1, mul_mem' := h.2.1, inv_mem' := h.2.2}, rfl⟩
Lifting Condition for Subgroups from Subsets
Informal description
For any group $G$, a subset $s$ of $G$ can be lifted to a subgroup of $G$ if and only if $s$ contains the identity element, is closed under multiplication, and is closed under taking inverses.
Subgroup.instSubgroupClass instance
: SubgroupClass (Subgroup G) G
Full source 
@[to_additive]
instance : SubgroupClass (Subgroup G) G where
  inv_mem := Subgroup.inv_mem' _
  one_mem _ := (Subgroup.toSubmonoid _).one_mem'
  mul_mem := (Subgroup.toSubmonoid _).mul_mem'
Subgroups Form a Subgroup Class
Informal description
For any group $G$, the type of subgroups of $G$ forms a `SubgroupClass`, meaning that every subgroup is closed under the group operations (multiplication, inversion) and contains the identity element.
Subgroup.mem_carrier theorem
{s : Subgroup G} {x : G} : x ∈ s.carrier ↔ x ∈ s
Full source 
@[to_additive]
theorem mem_carrier {s : Subgroup G} {x : G} : x ∈ s.carrierx ∈ s.carrier ↔ x ∈ s :=
  Iff.rfl
Membership in Subgroup Carrier Set
Informal description
For any subgroup $s$ of a group $G$ and any element $x \in G$, the element $x$ belongs to the underlying set of $s$ (denoted by `s.carrier`) if and only if $x$ is a member of the subgroup $s$.
Subgroup.mem_mk theorem
{s : Set G} {x : G} (h_one) (h_mul) (h_inv) : x ∈ mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ↔ x ∈ s
Full source 
@[to_additive (attr := simp)]
theorem mem_mk {s : Set G} {x : G} (h_one) (h_mul) (h_inv) :
    x ∈ mk ⟨⟨s, h_one⟩, h_mul⟩ h_invx ∈ mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ↔ x ∈ s :=
  Iff.rfl
Membership in Generated Subgroup
Informal description
For any subset $s$ of a group $G$ and any element $x \in G$, if $s$ is equipped with proofs that it contains the identity element ($h\_one$), is closed under multiplication ($h\_mul$), and is closed under taking inverses ($h\_inv$), then $x$ belongs to the subgroup generated by $s$ if and only if $x \in s$.
Subgroup.coe_set_mk theorem
{s : Set G} (h_one) (h_mul) (h_inv) : (mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv : Set G) = s
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_set_mk {s : Set G} (h_one) (h_mul) (h_inv) :
    (mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv : Set G) = s :=
  rfl
Subgroup Construction Preserves Underlying Set
Informal description
For any subset $s$ of a group $G$ that satisfies the subgroup axioms (closure under the identity, multiplication, and inverses), the underlying set of the constructed subgroup is equal to $s$. In other words, if $s$ is a subgroup of $G$ with identity closure $h\_one$, multiplication closure $h\_mul$, and inverse closure $h\_inv$, then the set of elements of the subgroup $\text{mk} \langle \langle s, h\_one \rangle, h\_mul \rangle h\_inv$ is equal to $s$.
Subgroup.mk_le_mk theorem
{s t : Set G} (h_one) (h_mul) (h_inv) (h_one') (h_mul') (h_inv') : mk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ≤ mk ⟨⟨t, h_one'⟩, h_mul'⟩ h_inv' ↔ s ⊆ t
Full source 
@[to_additive (attr := simp)]
theorem mk_le_mk {s t : Set G} (h_one) (h_mul) (h_inv) (h_one') (h_mul') (h_inv') :
    mkmk ⟨⟨s, h_one⟩, h_mul⟩ h_inv ≤ mk ⟨⟨t, h_one'⟩, h_mul'⟩ h_inv' ↔ s ⊆ t :=
  Iff.rfl
Subgroup Inclusion via Subset Relation
Informal description
For any two subsets $s$ and $t$ of a group $G$ that satisfy the subgroup axioms (closure under the identity, multiplication, and inverses), the subgroup generated by $s$ is contained in the subgroup generated by $t$ if and only if $s$ is a subset of $t$. More precisely, given: - Subgroup axioms for $s$: $h_{\text{one}}$ (contains identity), $h_{\text{mul}}$ (closed under multiplication), $h_{\text{inv}}$ (closed under inverses) - Subgroup axioms for $t$: $h'_{\text{one}}$, $h'_{\text{mul}}$, $h'_{\text{inv}}$ Then: \[ \text{mk}\langle\langle s, h_{\text{one}}\rangle, h_{\text{mul}}\rangle h_{\text{inv}} \leq \text{mk}\langle\langle t, h'_{\text{one}}\rangle, h'_{\text{mul}}\rangle h'_{\text{inv}} \leftrightarrow s \subseteq t \]
Subgroup.coe_toSubmonoid theorem
(K : Subgroup G) : (K.toSubmonoid : Set G) = K
Full source 
@[to_additive (attr := simp)]
theorem coe_toSubmonoid (K : Subgroup G) : (K.toSubmonoid : Set G) = K :=
  rfl
Subgroup to Submonoid Set Equality
Informal description
For any subgroup $K$ of a group $G$, the underlying set of the submonoid associated with $K$ is equal to the underlying set of $K$ itself.
Subgroup.mem_toSubmonoid theorem
(K : Subgroup G) (x : G) : x ∈ K.toSubmonoid ↔ x ∈ K
Full source 
@[to_additive (attr := simp)]
theorem mem_toSubmonoid (K : Subgroup G) (x : G) : x ∈ K.toSubmonoidx ∈ K.toSubmonoid ↔ x ∈ K :=
  Iff.rfl
Membership in Subgroup and its Underlying Submonoid Coincide
Informal description
For any subgroup $K$ of a group $G$ and any element $x \in G$, the element $x$ belongs to the underlying submonoid of $K$ if and only if $x$ belongs to $K$.
Subgroup.toSubmonoid_injective theorem
: Function.Injective (toSubmonoid : Subgroup G → Submonoid G)
Full source 
@[to_additive]
theorem toSubmonoid_injective : Function.Injective (toSubmonoid : Subgroup G → Submonoid G) :=
  -- fun p q h => SetLike.ext'_iff.2 (show _ from SetLike.ext'_iff.1 h)
  fun p q h => by
    have := SetLike.ext'_iff.1 h
    rw [coe_toSubmonoid, coe_toSubmonoid] at this
    exact SetLike.ext'_iff.2 this
Injectivity of the Subgroup-to-Submonoid Map
Informal description
The function that maps a subgroup $K$ of a group $G$ to its underlying submonoid is injective. That is, if two subgroups $K_1$ and $K_2$ of $G$ have the same underlying submonoid, then $K_1 = K_2$.
Subgroup.toSubmonoid_strictMono theorem
: StrictMono (toSubmonoid : Subgroup G → Submonoid G)
Full source 
@[to_additive (attr := mono)]
theorem toSubmonoid_strictMono : StrictMono (toSubmonoid : Subgroup G → Submonoid G) := fun _ _ =>
  id
Strict Monotonicity of Subgroup-to-Submonoid Map
Informal description
The function that maps a subgroup $H$ of a group $G$ to its underlying submonoid is strictly monotone. That is, for any two subgroups $H_1$ and $H_2$ of $G$, if $H_1 < H_2$ (meaning $H_1$ is a proper subgroup of $H_2$), then the underlying submonoid of $H_1$ is strictly contained in the underlying submonoid of $H_2$.
Subgroup.toSubmonoid_mono theorem
: Monotone (toSubmonoid : Subgroup G → Submonoid G)
Full source 
@[to_additive (attr := mono)]
theorem toSubmonoid_mono : Monotone (toSubmonoid : Subgroup G → Submonoid G) :=
  toSubmonoid_strictMono.monotone
Monotonicity of Subgroup-to-Submonoid Map
Informal description
The function that maps a subgroup $H$ of a group $G$ to its underlying submonoid is monotone. That is, for any two subgroups $H_1$ and $H_2$ of $G$, if $H_1 \leq H_2$ (meaning $H_1$ is a subgroup of $H_2$), then the underlying submonoid of $H_1$ is contained in the underlying submonoid of $H_2$.
Subgroup.toSubmonoid_le theorem
{p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q
Full source 
@[to_additive (attr := simp)]
theorem toSubmonoid_le {p q : Subgroup G} : p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q :=
  Iff.rfl
Subgroup containment via submonoid containment
Informal description
For any two subgroups $p$ and $q$ of a group $G$, the submonoid associated with $p$ is contained in the submonoid associated with $q$ if and only if $p$ is contained in $q$ as subgroups.
Subgroup.coe_nonempty theorem
(s : Subgroup G) : (s : Set G).Nonempty
Full source 
@[to_additive (attr := simp)]
lemma coe_nonempty (s : Subgroup G) : (s : Set G).Nonempty := ⟨1, one_mem _⟩
Nonemptiness of Subgroup Carrier Sets
Informal description
For any subgroup $s$ of a group $G$, the underlying set of $s$ is nonempty. That is, there exists at least one element $x \in G$ such that $x \in s$.
Subgroup.copy definition
(K : Subgroup G) (s : Set G) (hs : s = K) : Subgroup G
Full source 
/-- Copy of a subgroup with a new `carrier` equal to the old one. Useful to fix definitional
equalities. -/
@[to_additive (attr := simps)
      "Copy of an additive subgroup with a new `carrier` equal to the old one.
      Useful to fix definitional equalities"]
protected def copy (K : Subgroup G) (s : Set G) (hs : s = K) : Subgroup G where
  carrier := s
  one_mem' := hs.symm ▸ K.one_mem'
  mul_mem' := hs.symm ▸ K.mul_mem'
  inv_mem' hx := by simpa [hs] using hx
Copy of a subgroup with a specified carrier set
Informal description
Given a subgroup $K$ of a group $G$ and a subset $s$ of $G$ that is equal to the underlying set of $K$, the function `Subgroup.copy` constructs a new subgroup with $s$ as its underlying set. The new subgroup has the same group structure as $K$, including the same identity element, multiplication operation, and inverse operation.
Subgroup.copy_eq theorem
(K : Subgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K
Full source 
@[to_additive]
theorem copy_eq (K : Subgroup G) (s : Set G) (hs : s = ↑K) : K.copy s hs = K :=
  SetLike.coe_injective hs
Copy of Subgroup with Same Carrier is Original Subgroup
Informal description
Let $G$ be a group and $K$ a subgroup of $G$. For any subset $s$ of $G$ that equals the underlying set of $K$, the subgroup $K.\text{copy}(s, hs)$ is equal to $K$.
Subgroup.ext theorem
{H K : Subgroup G} (h : ∀ x, x ∈ H ↔ x ∈ K) : H = K
Full source 
/-- Two subgroups are equal if they have the same elements. -/
@[to_additive (attr := ext) "Two `AddSubgroup`s are equal if they have the same elements."]
theorem ext {H K : Subgroup G} (h : ∀ x, x ∈ Hx ∈ H ↔ x ∈ K) : H = K :=
  SetLike.ext h
Subgroup Extensionality: $H = K \iff \forall x \in G, x \in H \leftrightarrow x \in K$
Informal description
Two subgroups $H$ and $K$ of a group $G$ are equal if and only if they contain the same elements, i.e., for every $x \in G$, $x \in H$ if and only if $x \in K$.
Subgroup.one_mem theorem
: (1 : G) ∈ H
Full source 
/-- A subgroup contains the group's 1. -/
@[to_additive "An `AddSubgroup` contains the group's 0."]
protected theorem one_mem : (1 : G) ∈ H :=
  one_mem _
Identity Element Belongs to Every Subgroup
Informal description
For any subgroup $H$ of a group $G$, the identity element $1$ of $G$ is contained in $H$.
Subgroup.mul_mem theorem
{x y : G} : x ∈ H → y ∈ H → x * y ∈ H
Full source 
/-- A subgroup is closed under multiplication. -/
@[to_additive "An `AddSubgroup` is closed under addition."]
protected theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H :=
  mul_mem
Closure of Subgroup under Multiplication
Informal description
For any subgroup $H$ of a group $G$ and any elements $x, y \in G$, if $x \in H$ and $y \in H$, then their product $x * y$ also belongs to $H$.
Subgroup.inv_mem theorem
{x : G} : x ∈ H → x⁻¹ ∈ H
Full source 
/-- A subgroup is closed under inverse. -/
@[to_additive "An `AddSubgroup` is closed under inverse."]
protected theorem inv_mem {x : G} : x ∈ H → x⁻¹x⁻¹ ∈ H :=
  inv_mem
Inverse Closure Property of Subgroups
Informal description
For any element $x$ in a subgroup $H$ of a group $G$, the inverse $x^{-1}$ is also in $H$.
Subgroup.div_mem theorem
{x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H
Full source 
/-- A subgroup is closed under division. -/
@[to_additive "An `AddSubgroup` is closed under subtraction."]
protected theorem div_mem {x y : G} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H :=
  div_mem hx hy
Closure of Subgroup under Division
Informal description
Let $H$ be a subgroup of a group $G$. For any elements $x, y \in G$ such that $x \in H$ and $y \in H$, the quotient $x / y$ is also in $H$.
Subgroup.inv_mem_iff theorem
{x : G} : x⁻¹ ∈ H ↔ x ∈ H
Full source 
@[to_additive]
protected theorem inv_mem_iff {x : G} : x⁻¹x⁻¹ ∈ Hx⁻¹ ∈ H ↔ x ∈ H :=
  inv_mem_iff
Inversion Membership Criterion for Subgroups: $x^{-1} \in H \leftrightarrow x \in H$
Informal description
For any element $x$ in a group $G$ and any subgroup $H$ of $G$, the inverse $x^{-1}$ belongs to $H$ if and only if $x$ belongs to $H$.
Subgroup.exists_inv_mem_iff_exists_mem theorem
(K : Subgroup G) {P : G → Prop} : (∃ x : G, x ∈ K ∧ P x⁻¹) ↔ ∃ x ∈ K, P x
Full source 
@[to_additive]
protected theorem exists_inv_mem_iff_exists_mem (K : Subgroup G) {P : G → Prop} :
    (∃ x : G, x ∈ K ∧ P x⁻¹) ↔ ∃ x ∈ K, P x :=
  exists_inv_mem_iff_exists_mem
Existence of Inverse in Subgroup iff Existence of Element Satisfying Predicate
Informal description
For any subgroup $K$ of a group $G$ and any predicate $P$ on $G$, there exists an element $x \in G$ such that $x \in K$ and $P(x^{-1})$ holds if and only if there exists an element $x \in K$ such that $P(x)$ holds.
Subgroup.mul_mem_cancel_right theorem
{x y : G} (h : x ∈ H) : y * x ∈ H ↔ y ∈ H
Full source 
@[to_additive]
protected theorem mul_mem_cancel_right {x y : G} (h : x ∈ H) : y * x ∈ Hy * x ∈ H ↔ y ∈ H :=
  mul_mem_cancel_right h
Right Multiplication Cancellation in Subgroups: $y \cdot x \in H \leftrightarrow y \in H$ for $x \in H$
Informal description
Let $H$ be a subgroup of a group $G$. For any elements $x, y \in G$ with $x \in H$, we have $y \cdot x \in H$ if and only if $y \in H$.
Subgroup.mul_mem_cancel_left theorem
{x y : G} (h : x ∈ H) : x * y ∈ H ↔ y ∈ H
Full source 
@[to_additive]
protected theorem mul_mem_cancel_left {x y : G} (h : x ∈ H) : x * y ∈ Hx * y ∈ H ↔ y ∈ H :=
  mul_mem_cancel_left h
Left Multiplication Cancellation in Subgroups: $x \cdot y \in H \leftrightarrow y \in H$ for $x \in H$
Informal description
Let $H$ be a subgroup of a group $G$. For any elements $x, y \in G$ with $x \in H$, we have $x \cdot y \in H$ if and only if $y \in H$.
Subgroup.pow_mem theorem
{x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K
Full source 
@[to_additive]
protected theorem pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K :=
  pow_mem hx
Closure under Powers in Subgroups
Informal description
For any element $x$ in a subgroup $K$ of a group $G$, and for any natural number $n$, the power $x^n$ is also in $K$.
Subgroup.zpow_mem theorem
{x : G} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K
Full source 
@[to_additive]
protected theorem zpow_mem {x : G} (hx : x ∈ K) : ∀ n : ℤ, x ^ n ∈ K :=
  zpow_mem hx
Closure of Subgroups under Integer Powers: $x \in K \Rightarrow x^n \in K$ for all $n \in \mathbb{Z}$
Informal description
Let $G$ be a group and $K$ a subgroup of $G$. For any element $x \in K$ and any integer $n$, the power $x^n$ belongs to $K$.
Subgroup.ofDiv definition
(s : Set G) (hsn : s.Nonempty) (hs : ∀ᵉ (x ∈ s) (y ∈ s), x * y⁻¹ ∈ s) : Subgroup G
Full source 
/-- Construct a subgroup from a nonempty set that is closed under division. -/
@[to_additive "Construct a subgroup from a nonempty set that is closed under subtraction"]
def ofDiv (s : Set G) (hsn : s.Nonempty) (hs : ∀ᵉ (x ∈ s) (y ∈ s), x * y⁻¹ ∈ s) :
    Subgroup G :=
  have one_mem : (1 : G) ∈ s := by
    let ⟨x, hx⟩ := hsn
    simpa using hs x hx x hx
  have inv_mem : ∀ x, x ∈ s → x⁻¹x⁻¹ ∈ s := fun x hx => by simpa using hs 1 one_mem x hx
  { carrier := s
    one_mem' := one_mem
    inv_mem' := inv_mem _
    mul_mem' := fun hx hy => by simpa using hs _ hx _ (inv_mem _ hy) }
Subgroup construction from division-closed nonempty set
Informal description
Given a nonempty subset $s$ of a group $G$ that is closed under the operation $x * y^{-1}$ for any $x, y \in s$, the structure `Subgroup.ofDiv` constructs a subgroup of $G$ with carrier set $s$. Specifically: 1. The identity element $1$ is in $s$ (since $s$ is nonempty and closed under $x * y^{-1}$) 2. For any $x \in s$, its inverse $x^{-1}$ is also in $s$ 3. For any $x, y \in s$, their product $x * y$ is in $s$
Subgroup.mul instance
: Mul H
Full source 
/-- A subgroup of a group inherits a multiplication. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an addition."]
instance mul : Mul H :=
  H.toSubmonoid.mul
Multiplication Operation on Subgroups
Informal description
For any subgroup $H$ of a group $G$, the multiplication operation on $G$ restricts to a multiplication operation on $H$.
Subgroup.one instance
: One H
Full source 
/-- A subgroup of a group inherits a 1. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a zero."]
instance one : One H :=
  H.toSubmonoid.one
Subgroups Contain the Identity Element
Informal description
Every subgroup $H$ of a group $G$ contains the identity element of $G$.
Subgroup.inv instance
: Inv H
Full source 
/-- A subgroup of a group inherits an inverse. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an inverse."]
instance inv : Inv H :=
  ⟨fun a => ⟨a⁻¹, H.inv_mem a.2⟩⟩
Inversion in Subgroups
Informal description
For any subgroup $H$ of a group $G$, the inversion operation on $G$ restricts to an inversion operation on $H$.
Subgroup.div instance
: Div H
Full source 
/-- A subgroup of a group inherits a division -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits a subtraction."]
instance div : Div H :=
  ⟨fun a b => ⟨a / b, H.div_mem a.2 b.2⟩⟩
Subgroup Closure Under Division
Informal description
For any subgroup $H$ of a group $G$, the division operation $/$ on $G$ restricts to $H$, making $H$ closed under division.
AddSubgroup.nsmul instance
{G} [AddGroup G] {H : AddSubgroup G} : SMul ℕ H
Full source 
/-- An `AddSubgroup` of an `AddGroup` inherits a natural scaling. -/
instance _root_.AddSubgroup.nsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℕ H :=
  ⟨fun n a => ⟨n • a, H.nsmul_mem a.2 n⟩⟩
Natural Number Scalar Multiplication on Additive Subgroups
Informal description
For any additive group $G$ and additive subgroup $H$ of $G$, $H$ inherits a natural scalar multiplication by natural numbers, where for any $n \in \mathbb{N}$ and $h \in H$, the product $n \cdot h$ is defined as the $n$-fold sum of $h$ in $H$.
Subgroup.npow instance
: Pow H ℕ
Full source 
/-- A subgroup of a group inherits a natural power -/
@[to_additive existing]
protected instance npow : Pow H ℕ :=
  ⟨fun a n => ⟨a ^ n, H.pow_mem a.2 n⟩⟩
Natural Number Power Operation on Subgroups
Informal description
For any subgroup $H$ of a group $G$, there is a natural power operation $H \times \mathbb{N} \to H$ defined by repeated multiplication within the subgroup, where $x^n = x \cdot \cdots \cdot x$ ($n$ times) for $x \in H$.
AddSubgroup.zsmul instance
{G} [AddGroup G] {H : AddSubgroup G} : SMul ℤ H
Full source 
/-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling. -/
instance _root_.AddSubgroup.zsmul {G} [AddGroup G] {H : AddSubgroup G} : SMul ℤ H :=
  ⟨fun n a => ⟨n • a, H.zsmul_mem a.2 n⟩⟩
Integer Scalar Multiplication on Additive Subgroups
Informal description
For any additive group $G$ and additive subgroup $H$ of $G$, $H$ inherits a scalar multiplication operation by integers from $G$.
Subgroup.zpow instance
: Pow H ℤ
Full source 
/-- A subgroup of a group inherits an integer power -/
@[to_additive existing]
instance zpow : Pow H ℤ :=
  ⟨fun a n => ⟨a ^ n, H.zpow_mem a.2 n⟩⟩
Subgroups are Closed Under Integer Powers
Informal description
For any subgroup $H$ of a group $G$, the integer power operation on $G$ restricts to an integer power operation on $H$. That is, for any $h \in H$ and $n \in \mathbb{Z}$, we have $h^n \in H$.
Subgroup.coe_mul theorem
(x y : H) : (↑(x * y) : G) = ↑x * ↑y
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_mul (x y : H) : (↑(x * y) : G) = ↑x * ↑y :=
  rfl
Subgroup Multiplication Preserves Inclusion
Informal description
For any elements $x$ and $y$ in a subgroup $H$ of a group $G$, the canonical inclusion of their product in $G$ equals the product of their inclusions, i.e., $(x \cdot y) = x \cdot y$ where the left-hand side is interpreted in $H$ and the right-hand side in $G$.
Subgroup.coe_one theorem
: ((1 : H) : G) = 1
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_one : ((1 : H) : G) = 1 :=
  rfl
Subgroup Identity Coincides with Group Identity
Informal description
For any subgroup $H$ of a group $G$, the canonical inclusion of the identity element $1_H$ of $H$ into $G$ equals the identity element $1_G$ of $G$, i.e., $1_H = 1_G$ when viewed in $G$.
Subgroup.coe_inv theorem
(x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G)
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G) :=
  rfl
Subgroup Inversion Preserved Under Coercion
Informal description
For any element $x$ in a subgroup $H$ of a group $G$, the inverse of $x$ in $H$ (denoted $x^{-1}$) is equal to the inverse of $x$ in $G$ when both are viewed as elements of $G$.
Subgroup.coe_div theorem
(x y : H) : (↑(x / y) : G) = ↑x / ↑y
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_div (x y : H) : (↑(x / y) : G) = ↑x / ↑y :=
  rfl
Subgroup Division Coercion Compatibility
Informal description
For any elements $x$ and $y$ in a subgroup $H$ of a group $G$, the coercion of the quotient $x / y$ in $H$ to $G$ equals the quotient of the coercions of $x$ and $y$ in $G$, i.e., $(x / y : G) = (x : G) / (y : G)$.
Subgroup.coe_mk theorem
(x : G) (hx : x ∈ H) : ((⟨x, hx⟩ : H) : G) = x
Full source 
@[to_additive (attr := norm_cast)]
theorem coe_mk (x : G) (hx : x ∈ H) : ((⟨x, hx⟩ : H) : G) = x :=
  rfl
Subgroup Element Coercion Preserves Identity
Informal description
For any element $x$ in a group $G$ and any subgroup $H$ of $G$, if $x$ belongs to $H$, then the canonical inclusion of the subgroup element $\langle x, hx \rangle$ (where $hx$ is the proof that $x \in H$) into $G$ is equal to $x$ itself. In other words, the coercion of the subgroup element back to the ambient group preserves the original element.
Subgroup.coe_pow theorem
(x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n
Full source 
@[to_additive (attr := simp, norm_cast)]
theorem coe_pow (x : H) (n : ℕ) : ((x ^ n : H) : G) = (x : G) ^ n :=
  rfl
Subgroup Power Preservation: $(x^n)_H = x^n_G$ for $x \in H \leq G$ and $n \in \mathbb{N}$
Informal description
For any element $x$ in a subgroup $H$ of a group $G$ and any natural number $n$, the $n$-th power of $x$ in $H$ (denoted $x^n$) coincides with the $n$-th power of $x$ in $G$ when both are viewed as elements of $G$. In other words, the canonical inclusion map from $H$ to $G$ preserves powers.
Subgroup.coe_zpow theorem
(x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n
Full source 
@[to_additive (attr := norm_cast)]
theorem coe_zpow (x : H) (n : ℤ) : ((x ^ n : H) : G) = (x : G) ^ n := by
  dsimp
Subgroup Integer Power Coercion: $(x^n : H) = (x : G)^n$
Informal description
For any element $x$ in a subgroup $H$ of a group $G$ and any integer $n$, the canonical inclusion of the integer power $x^n$ in $H$ into $G$ is equal to the integer power of the inclusion of $x$ in $G$ raised to $n$. In other words, $(x^n : H) = (x : G)^n$ under the inclusion map.
Subgroup.mk_eq_one theorem
{g : G} {h} : (⟨g, h⟩ : H) = 1 ↔ g = 1
Full source 
@[to_additive (attr := simp)]
theorem mk_eq_one {g : G} {h} : (⟨g, h⟩ : H) = 1 ↔ g = 1 := Submonoid.mk_eq_one ..
Subgroup Element Equals Identity iff Underlying Element Equals Identity
Informal description
For any element $g$ in a group $G$ and a proof $h$ that $g$ belongs to a subgroup $H$ of $G$, the subgroup element $\langle g, h \rangle$ is equal to the identity element $1$ of $H$ if and only if $g$ is equal to the identity element $1$ of $G$.
Subgroup.toGroup instance
{G : Type*} [Group G] (H : Subgroup G) : Group H
Full source 
/-- A subgroup of a group inherits a group structure. -/
@[to_additive "An `AddSubgroup` of an `AddGroup` inherits an `AddGroup` structure."]
instance toGroup {G : Type*} [Group G] (H : Subgroup G) : Group H := fast_instance%
  Subtype.coe_injective.group _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Subgroup Inherits Group Structure
Informal description
For any group $G$ and subgroup $H$ of $G$, $H$ inherits a group structure from $G$. This means $H$ is equipped with a multiplication operation, an identity element, and an inversion operation, satisfying the group axioms.
Subgroup.toCommGroup instance
{G : Type*} [CommGroup G] (H : Subgroup G) : CommGroup H
Full source 
/-- A subgroup of a `CommGroup` is a `CommGroup`. -/
@[to_additive "An `AddSubgroup` of an `AddCommGroup` is an `AddCommGroup`."]
instance toCommGroup {G : Type*} [CommGroup G] (H : Subgroup G) : CommGroup H := fast_instance%
  Subtype.coe_injective.commGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl
Subgroups of Commutative Groups are Commutative
Informal description
For any commutative group $G$ and any subgroup $H$ of $G$, $H$ inherits a commutative group structure from $G$.
Subgroup.subtype definition
: H →* G
Full source 
/-- The natural group hom from a subgroup of group `G` to `G`. -/
@[to_additive "The natural group hom from an `AddSubgroup` of `AddGroup` `G` to `G`."]
protected def subtype : H →* G where
  toFun := ((↑) : H → G); map_one' := rfl; map_mul' _ _ := rfl
Subgroup inclusion homomorphism
Informal description
The natural group homomorphism from a subgroup $H$ of a group $G$ to $G$ itself, which maps each element of $H$ to its corresponding element in $G$. This homomorphism preserves the group structure, meaning it maps the identity element of $H$ to the identity element of $G$ and respects the group operation (i.e., $\text{subtype}(x \cdot y) = \text{subtype}(x) \cdot \text{subtype}(y)$ for any $x, y \in H$).
Subgroup.subtype_apply theorem
{s : Subgroup G} (x : s) : s.subtype x = x
Full source 
@[to_additive (attr := simp)]
lemma subtype_apply {s : Subgroup G} (x : s) :
    s.subtype x = x := rfl
Subgroup Inclusion Homomorphism Acts as Identity on Elements
Informal description
For any subgroup $H$ of a group $G$ and any element $x \in H$, the subgroup inclusion homomorphism $\text{subtype}$ maps $x$ to itself when viewed as an element of $G$, i.e., $\text{subtype}(x) = x$.
Subgroup.subtype_injective theorem
(s : Subgroup G) : Function.Injective s.subtype
Full source 
@[to_additive]
lemma subtype_injective (s : Subgroup G) :
    Function.Injective s.subtype :=
  Subtype.coe_injective
Injectivity of Subgroup Inclusion Homomorphism
Informal description
For any subgroup $H$ of a group $G$, the inclusion homomorphism $\text{subtype} \colon H \to G$ is injective. That is, if $\text{subtype}(x) = \text{subtype}(y)$ for $x, y \in H$, then $x = y$.
Subgroup.coe_subtype theorem
: ⇑H.subtype = ((↑) : H → G)
Full source 
@[to_additive (attr := simp)]
theorem coe_subtype : ⇑ H.subtype = ((↑) : H → G) :=
  rfl
Subgroup Inclusion Homomorphism Equals Coercion
Informal description
The underlying function of the subgroup inclusion homomorphism $H \to G$ is equal to the coercion function from the subgroup $H$ to the group $G$.
Subgroup.inclusion definition
{H K : Subgroup G} (h : H ≤ K) : H →* K
Full source 
/-- The inclusion homomorphism from a subgroup `H` contained in `K` to `K`. -/
@[to_additive "The inclusion homomorphism from an additive subgroup `H` contained in `K` to `K`."]
def inclusion {H K : Subgroup G} (h : H ≤ K) : H →* K :=
  MonoidHom.mk' (fun x => ⟨x, h x.2⟩) fun _ _ => rfl
Inclusion homomorphism between subgroups
Informal description
Given two subgroups \( H \) and \( K \) of a group \( G \) such that \( H \) is contained in \( K \) (denoted \( H \leq K \)), the inclusion homomorphism is the group homomorphism from \( H \) to \( K \) that maps each element \( x \in H \) to itself (viewed as an element of \( K \)).
Subgroup.coe_inclusion theorem
{H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a
Full source 
@[to_additive (attr := simp)]
theorem coe_inclusion {H K : Subgroup G} {h : H ≤ K} (a : H) : (inclusion h a : G) = a := by
  cases a
  simp only [inclusion, coe_mk, MonoidHom.mk'_apply]
Inclusion Homomorphism Preserves Elements: $(\text{inclusion}\, h)(a) = a$
Informal description
Let $G$ be a group and let $H$ and $K$ be subgroups of $G$ such that $H \leq K$. For any element $a \in H$, the image of $a$ under the inclusion homomorphism $\text{inclusion}\, h \colon H \to K$ (viewed as an element of $G$) equals $a$ itself, i.e., $(\text{inclusion}\, h)(a) = a$.
Subgroup.inclusion_injective theorem
{H K : Subgroup G} (h : H ≤ K) : Function.Injective <| inclusion h
Full source 
@[to_additive]
theorem inclusion_injective {H K : Subgroup G} (h : H ≤ K) : Function.Injective <| inclusion h :=
  Set.inclusion_injective h
Injectivity of Subgroup Inclusion Homomorphism
Informal description
Let $G$ be a group and let $H$ and $K$ be subgroups of $G$ such that $H \leq K$. Then the inclusion homomorphism $\text{inclusion}(h) : H \to K$ is injective.
Subgroup.inclusion_inj theorem
{H K : Subgroup G} (h : H ≤ K) {x y : H} : inclusion h x = inclusion h y ↔ x = y
Full source 
@[to_additive (attr := simp)]
lemma inclusion_inj {H K : Subgroup G} (h : H ≤ K) {x y : H} :
    inclusioninclusion h x = inclusion h y ↔ x = y :=
  (inclusion_injective h).eq_iff
Inclusion Homomorphism is Injective: $\text{inclusion}(h)(x) = \text{inclusion}(h)(y) \leftrightarrow x = y$
Informal description
Let $G$ be a group and let $H$ and $K$ be subgroups of $G$ such that $H \leq K$. For any elements $x, y \in H$, the inclusion homomorphism $\text{inclusion}(h) : H \to K$ satisfies $\text{inclusion}(h)(x) = \text{inclusion}(h)(y)$ if and only if $x = y$.
Subgroup.subtype_comp_inclusion theorem
{H K : Subgroup G} (hH : H ≤ K) : K.subtype.comp (inclusion hH) = H.subtype
Full source 
@[to_additive (attr := simp)]
theorem subtype_comp_inclusion {H K : Subgroup G} (hH : H ≤ K) :
    K.subtype.comp (inclusion hH) = H.subtype :=
  rfl
Compatibility of Subgroup Inclusion and Subtype Homomorphisms
Informal description
Let $G$ be a group with subgroups $H$ and $K$ such that $H \leq K$. Then the composition of the inclusion homomorphism from $H$ to $K$ with the subgroup inclusion homomorphism from $K$ to $G$ equals the subgroup inclusion homomorphism from $H$ to $G$. In other words, the following diagram commutes: \[ \begin{tikzcd} H \arrow[r, "\text{inclusion}"] \arrow[rr, bend right=30, "\text{subtype}"'] & K \arrow[r, "\text{subtype}"] & G \end{tikzcd} \]
Subgroup.Normal structure
Full source 
/-- A subgroup is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` -/
structure Normal : Prop where
  /-- `N` is closed under conjugation -/
  conj_mem : ∀ n, n ∈ H → ∀ g : G, g * n * g⁻¹ ∈ H
Normal subgroup
Informal description
A subgroup $H$ of a group $G$ is called normal if for every element $n \in H$ and every element $g \in G$, the conjugate $g * n * g^{-1}$ belongs to $H$.
AddSubgroup.Normal structure
(H : AddSubgroup A)
Full source 
/-- An AddSubgroup is normal if whenever `n ∈ H`, then `g + n - g ∈ H` for every `g : G` -/
structure Normal (H : AddSubgroup A) : Prop where
  /-- `N` is closed under additive conjugation -/
  conj_mem : ∀ n, n ∈ H → ∀ g : A, g + n + -g ∈ H
Normal additive subgroup
Informal description
An additive subgroup $H$ of an additive group $A$ is called normal if for every element $n \in H$ and every element $g \in A$, the element $g + n - g$ belongs to $H$.
Subgroup.normal_of_comm instance
{G : Type*} [CommGroup G] (H : Subgroup G) : H.Normal
Full source 
@[to_additive]
instance (priority := 100) normal_of_comm {G : Type*} [CommGroup G] (H : Subgroup G) : H.Normal :=
  ⟨by simp [mul_comm, mul_left_comm]⟩
Subgroups of Commutative Groups are Normal
Informal description
For any commutative group $G$ and any subgroup $H$ of $G$, $H$ is a normal subgroup. That is, for every $n \in H$ and $g \in G$, the conjugate $g^{-1} * n * g$ belongs to $H$.
Subgroup.Normal.conj_mem' theorem
(nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) : g⁻¹ * n * g ∈ H
Full source 
@[to_additive]
theorem conj_mem' (nH : H.Normal) (n : G) (hn : n ∈ H) (g : G) :
    g⁻¹g⁻¹ * n * g ∈ H := by
  convert nH.conj_mem n hn g⁻¹
  rw [inv_inv]
Conjugate of Normal Subgroup Element is in Subgroup
Informal description
Let $H$ be a normal subgroup of a group $G$. For any element $n \in H$ and any element $g \in G$, the conjugate $g^{-1} * n * g$ is also in $H$.
Subgroup.Normal.mem_comm_iff theorem
(nH : H.Normal) {a b : G} : a * b ∈ H ↔ b * a ∈ H
Full source 
@[to_additive]
theorem mem_comm_iff (nH : H.Normal) {a b : G} : a * b ∈ Ha * b ∈ H ↔ b * a ∈ H :=
  ⟨nH.mem_comm, nH.mem_comm⟩
Commutativity of Products Modulo a Normal Subgroup
Informal description
Let $H$ be a normal subgroup of a group $G$. For any elements $a, b \in G$, the product $a \cdot b$ belongs to $H$ if and only if the product $b \cdot a$ belongs to $H$.
Subgroup.normalizer definition
: Subgroup G
Full source 
/-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/
@[to_additive "The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal."]
def normalizer : Subgroup G where
  carrier := { g : G | ∀ n, n ∈ H ↔ g * n * g⁻¹ ∈ H }
  one_mem' := by simp
  mul_mem' {a b} (ha : ∀ n, n ∈ Hn ∈ H ↔ a * n * a⁻¹ ∈ H) (hb : ∀ n, n ∈ Hn ∈ H ↔ b * n * b⁻¹ ∈ H) n := by
    rw [hb, ha]
    simp only [mul_assoc, mul_inv_rev]
  inv_mem' {a} (ha : ∀ n, n ∈ Hn ∈ H ↔ a * n * a⁻¹ ∈ H) n := by
    rw [ha (a⁻¹ * n * a⁻¹a⁻¹⁻¹)]
    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
Normalizer of a subgroup
Informal description
The normalizer of a subgroup $H$ of a group $G$ is the subgroup of $G$ consisting of all elements $g \in G$ such that for every $n \in G$, $n \in H$ if and only if $g * n * g^{-1} \in H$. In other words, the normalizer is the largest subgroup of $G$ in which $H$ is normal.
Subgroup.setNormalizer definition
(S : Set G) : Subgroup G
Full source 
/-- The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy `g*S*g⁻¹=S` -/
@[to_additive
      "The `setNormalizer` of `S` is the subgroup of `G` whose elements satisfy
      `g+S-g=S`."]
def setNormalizer (S : Set G) : Subgroup G where
  carrier := { g : G | ∀ n, n ∈ S ↔ g * n * g⁻¹ ∈ S }
  one_mem' := by simp
  mul_mem' {a b} (ha : ∀ n, n ∈ Sn ∈ S ↔ a * n * a⁻¹ ∈ S) (hb : ∀ n, n ∈ Sn ∈ S ↔ b * n * b⁻¹ ∈ S) n := by
    rw [hb, ha]
    simp only [mul_assoc, mul_inv_rev]
  inv_mem' {a} (ha : ∀ n, n ∈ Sn ∈ S ↔ a * n * a⁻¹ ∈ S) n := by
    rw [ha (a⁻¹ * n * a⁻¹a⁻¹⁻¹)]
    simp only [inv_inv, mul_assoc, mul_inv_cancel_left, mul_inv_cancel, mul_one]
Set normalizer of a subset in a group
Informal description
For a subset $S$ of a group $G$, the *set normalizer* of $S$ is the subgroup of $G$ consisting of all elements $g \in G$ such that conjugation by $g$ preserves $S$, i.e., $g * n * g^{-1} \in S$ if and only if $n \in S$ for every $n \in G$.
Subgroup.mem_normalizer_iff theorem
{g : G} : g ∈ H.normalizer ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H
Full source 
@[to_additive]
theorem mem_normalizer_iff {g : G} : g ∈ H.normalizerg ∈ H.normalizer ↔ ∀ h, h ∈ H ↔ g * h * g⁻¹ ∈ H :=
  Iff.rfl
Characterization of Normalizer Membership via Conjugation
Informal description
For any element $g$ in a group $G$, $g$ belongs to the normalizer of a subgroup $H$ if and only if for every element $h \in G$, $h$ is in $H$ precisely when the conjugate $g h g^{-1}$ is in $H$.
Subgroup.mem_normalizer_iff'' theorem
{g : G} : g ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H
Full source 
@[to_additive]
theorem mem_normalizer_iff'' {g : G} : g ∈ H.normalizerg ∈ H.normalizer ↔ ∀ h : G, h ∈ H ↔ g⁻¹ * h * g ∈ H := by
  rw [← inv_mem_iff (x := g), mem_normalizer_iff, inv_inv]
Characterization of Normalizer Membership via Conjugation with Inverse: $g \in N_G(H) \leftrightarrow (\forall h \in G, h \in H \leftrightarrow g^{-1} h g \in H)$
Informal description
For any element $g$ in a group $G$, $g$ belongs to the normalizer of a subgroup $H$ if and only if for every element $h \in G$, $h$ is in $H$ precisely when the conjugate $g^{-1} h g$ is in $H$.
Subgroup.mem_normalizer_iff' theorem
{g : G} : g ∈ H.normalizer ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H
Full source 
@[to_additive]
theorem mem_normalizer_iff' {g : G} : g ∈ H.normalizerg ∈ H.normalizer ↔ ∀ n, n * g ∈ H ↔ g * n ∈ H :=
  ⟨fun h n => by rw [h, mul_assoc, mul_inv_cancel_right], fun h n => by
    rw [mul_assoc, ← h, inv_mul_cancel_right]⟩
Characterization of Normalizer Membership via Left and Right Multiplication
Informal description
For any element $g$ in a group $G$, $g$ belongs to the normalizer of a subgroup $H$ if and only if for every element $n \in G$, the product $n \cdot g$ is in $H$ precisely when $g \cdot n$ is in $H$.
Subgroup.commGroup_isMulCommutative instance
{G : Type*} [CommGroup G] (H : Subgroup G) : IsMulCommutative H
Full source 
/-- A subgroup of a commutative group is commutative. -/
@[to_additive "A subgroup of a commutative group is commutative."]
instance commGroup_isMulCommutative {G : Type*} [CommGroup G] (H : Subgroup G) :
    IsMulCommutative H :=
  ⟨CommMagma.to_isCommutative⟩
Subgroups of Commutative Groups are Commutative
Informal description
For any commutative group $G$ and any subgroup $H$ of $G$, the multiplication operation on $H$ is commutative.
Subgroup.mul_comm_of_mem_isMulCommutative theorem
[IsMulCommutative H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) : a * b = b * a
Full source 
@[to_additive]
lemma mul_comm_of_mem_isMulCommutative [IsMulCommutative H] {a b : G} (ha : a ∈ H) (hb : b ∈ H) :
    a * b = b * a := by
  simpa only [MulMemClass.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H)
Commutativity in Subgroups with Commutative Multiplication
Informal description
Let $H$ be a subgroup of a group $G$ with a commutative multiplication operation. For any elements $a, b \in G$ that belong to $H$, we have $a \cdot b = b \cdot a$.