Theorems · Definition · group theory

Subgroup.quotientiInfSubgroupOfEmbedding

{α : Type u_1} →
  [inst : Group α] →
    {ι : Type u_2} →
      (f : ι → Subgroup α) → (H : Subgroup α) → ↥H ⧸ (⨅ i, f i).subgroupOf H ↪ (i : ι) → ↥H ⧸ (f i).subgroupOf H

The natural embedding H ⧸ (⨅ i, f i).subgroupOf H ↪ Π i, H ⧸ (f i).subgroupOf H.

Defined in: Mathlib.GroupTheory.Coset.Basic
Cited by: 4 results in Mathlib
Foundations: Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Groupstatement and proof · cited by 6,238
Subgroupstatement and proof · cited by 3,593
HasQuotient.Quotientstatement and proof · cited by 2,301
iInfstatement and proof · cited by 1,690
Function.Embeddingstatement · cited by 988
Subgroup.subgroupOfstatement and proof · cited by 122
Subgroup.quotientSubgroupOfMapOfLEproof · cited by 3

Cited by4

Results whose statement or proof uses this declaration.

Subgroup.relIndex_iInf_ne_zeroproof · cited by 1
Subgroup.relIndex_iInf_leproof · cited by 0
Subgroup.quotientiInfSubgroupOfEmbedding_applystatement and proof · cited by 0
Subgroup.quotientiInfSubgroupOfEmbedding_apply_mkstatement · cited by 0