ModuleSubgroups.lean
Nyll.ProCGroups.GroupTheory.Subgroups
3 declarations indexed from sourceView source ↗ Module documentation
Quotients by kernels
This module realizes the quotient by the kernel of a homomorphism as an injective homomorphism into the target and records its value on quotient representatives.
Imports2
- Mathlib.GroupTheory.QuotientGroup.Basic
- Mathlib.Topology.Algebra.OpenSubgroup
Imported by2
Declarations
ProCGroups.GroupTheory.quotientKerEmbedding
DocumentationThe canonical embedding of a kernel quotient into the target range, viewed in the target.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]
ProCGroups.GroupTheory.quotientKerEmbedding_injective
DocumentationThe quotient-kernel embedding is injective.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]
ProCGroups.GroupTheory.quotientKerEmbedding_mk
DocumentationThe quotient-kernel embedding sends a representative to the corresponding kernel coset.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups.GroupTheory
universe u
variable {G : Type u} [Group G]