Loogle!

Result

Found 146 declarations mentioning Subgroup.subtype.

• Subgroup.subtype 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [Group G] (H : Subgroup G) : ↥H →* G
• Subgroup.subtype_injective 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [Group G] (s : Subgroup G) : Function.Injective ⇑s.subtype
• Subgroup.coe_subtype 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [Group G] (H : Subgroup G) : ⇑H.subtype = Subtype.val
• Subgroup.subtype_apply 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [Group G] {s : Subgroup G} (x : ↥s) : s.subtype x = ↑x
• Subgroup.subtype_comp_inclusion 📋 Mathlib.Algebra.Group.Subgroup.Defs
  {G : Type u_1} [Group G] {H K : Subgroup G} (hH : H ≤ K) : K.subtype.comp (Subgroup.inclusion hH) = H.subtype
• Subgroup.subgroupOf_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (H K : Subgroup G) : Subgroup.map K.subtype (H.subgroupOf K) = H ⊓ K
• Subgroup.map_subgroupOf_eq_of_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {H K : Subgroup G} (h : H ≤ K) : Subgroup.map K.subtype (H.subgroupOf K) = H
• Subgroup.comap_subtype 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (H K : Subgroup G) : Subgroup.comap K.subtype H = H.subgroupOf K
• Subgroup.coe_subgroupOf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] (H K : Subgroup G) : ↑(H.subgroupOf K) = ⇑K.subtype ⁻¹' ↑H
• Subgroup.range_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.range = H
• Subgroup.subtype_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.range = H
• Subgroup.map_subtype_le 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) : Subgroup.map H.subtype K ≤ H
• Subgroup.ker_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] (H : Subgroup G) : H.subtype.ker = ⊥
• Subgroup.map_subtype_inj 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {H : Subgroup G} {K L : Subgroup ↥H} : Subgroup.map H.subtype K = Subgroup.map H.subtype L ↔ K = L
• MonoidHom.subtype_comp_rangeRestrict 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {N : Type u_4} [Group N] (f : G →* N) : f.range.subtype.comp f.rangeRestrict = f
• Subgroup.map_subtype_le_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {G' : Subgroup G} {H K : Subgroup ↥G'} : Subgroup.map G'.subtype H ≤ Subgroup.map G'.subtype K ↔ H ≤ K
• Subgroup.map_subtype_lt_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {G' : Subgroup G} {H K : Subgroup ↥G'} : Subgroup.map G'.subtype H < Subgroup.map G'.subtype K ↔ H < K
• Subgroup.closure_preimage_eq_top 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.closure (⇑(Subgroup.closure s).subtype ⁻¹' s) = ⊤
• Subgroup.MapSubtype.orderIso_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] (H : Subgroup G) (H' : Subgroup ↥H) : ↑((Subgroup.MapSubtype.orderIso H) H') = Subgroup.map H.subtype H'
• Subgroup.Normal.of_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {K : Subgroup G} {L : Subgroup ↥K} (n : (Subgroup.map K.subtype L).Normal) : L.Normal
• Subgroup.characteristic_of_characteristic_of_characteristic 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {H : Subgroup G} [H.Characteristic] {K : Subgroup ↥H} [hK : K.Characteristic] : (Subgroup.map H.subtype K).Characteristic
• AddSubgroup.inertia_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {M : Type u_5} [AddGroup M] (I : AddSubgroup M) {G : Type u_6} [Group G] [MulAction G M] (H : Subgroup G) : Subgroup.map H.subtype (I.inertia ↥H) = I.inertia G ⊓ H
• ConjAct.normal_of_characteristic_of_normal 📋 Mathlib.GroupTheory.GroupAction.ConjAct
  {G : Type u_3} [Group G] {H : Subgroup G} [hH : H.Normal] {K : Subgroup ↥H} [h : K.Characteristic] : (Subgroup.map H.subtype K).Normal
• QuotientGroup.mk'_comp_subtype 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} [Group G] (N : Subgroup G) [nN : N.Normal] : (QuotientGroup.mk' N).comp N.subtype = 1
• QuotientGroup.ker_le_range_iff 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u_1} {H : Type u_2} {I : Type u_3} [Group G] [Group H] [MulOneClass I] (f : G →* H) [f.range.Normal] (g : H →* I) : g.ker ≤ f.range ↔ (QuotientGroup.mk' f.range).comp g.ker.subtype = 1
• Subgroup.map_subtype_commutator 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup.map H.subtype (commutator ↥H) = ⁅H, H⁆
• image_commutatorSet_closureCommutatorRepresentatives 📋 Mathlib.GroupTheory.Commutator.Basic
  (G : Type u_1) [Group G] : ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) = commutatorSet G
• Subgroup.card_subtype 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {G : Type u_1} [Group G] (K : Subgroup G) (L : Subgroup ↥K) : Nat.card ↥(Subgroup.map K.subtype L) = Nat.card ↥L
• QuotientGroup.strictMono_comap_prod_image 📋 Mathlib.GroupTheory.Coset.Basic
  {α : Type u_1} [Group α] (s : Subgroup α) : StrictMono fun t => (Subgroup.comap s.subtype t, QuotientGroup.mk '' ↑t)
• QuotientGroup.strictMono_comap_prod_map 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : StrictMono fun H => (Subgroup.comap N.subtype H, Subgroup.map (QuotientGroup.mk' N) H)
• Subgroup.exists_eq_graph 📋 Mathlib.Algebra.Group.Graph
  {H : Type u_2} {I : Type u_3} [Group H] [Group I] {G : Subgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) : ∃ f, G = f.graph
• Subgroup.exists_mulEquiv_eq_graph 📋 Mathlib.Algebra.Group.Graph
  {H : Type u_2} {I : Type u_3} [Group H] [Group I] {G : Subgroup (H × I)} (hG₁ : Function.Bijective (Prod.fst ∘ ⇑G.subtype)) (hG₂ : Function.Bijective (Prod.snd ∘ ⇑G.subtype)) : ∃ e, G = e.toMonoidHom.graph
• Function.MulExact.monoidHom_rangeRestrict 📋 Mathlib.Algebra.Exact.Basic
  {M : Type u_2} {N : Type u_4} {P : Type u_6} [Group M] [Group N] [Group P] {f : M →* N} {g : N →* P} : Function.MulExact ⇑f ⇑g → Function.MulExact ⇑f.range.subtype ⇑g.rangeRestrict
• Function.MulExact.iff_monoidHom_rangeRestrict 📋 Mathlib.Algebra.Exact.Basic
  {M : Type u_2} {N : Type u_4} {P : Type u_6} [Group M] [Group N] [Group P] {f : M →* N} {g : N →* P} : Function.MulExact ⇑f ⇑g ↔ Function.MulExact ⇑f.range.subtype ⇑g.rangeRestrict
• Subgroup.index_map_subtype 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [Group G] {H : Subgroup G} (K : Subgroup ↥H) : (Subgroup.map H.subtype K).index = K.index * H.index
• Subgroup.commute_subtype_of_commute 📋 Mathlib.GroupTheory.NoncommPiCoprod
  {G : Type u_1} [Group G] {ι : Type u_2} {H : ι → Subgroup G} (hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) (i j : ι) (hne : i ≠ j) (x : ↥(H i)) (y : ↥(H j)) : Commute ((H i).subtype x) ((H j).subtype y)
• Subgroup.properlyDiscontinuousSMul_opposite_of_tendsto_cofinite 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul (↥S.op) G
• Subgroup.properlyDiscontinuousSMul_of_tendsto_cofinite 📋 Mathlib.Topology.Algebra.Group.Subgroup
  {G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (S : Subgroup G) (hS : Filter.Tendsto (⇑S.subtype) Filter.cofinite (Filter.cocompact G)) : ProperlyDiscontinuousSMul (↥S) G
• Ideal.Quotient.map_ker_stabilizer_subtype 📋 Mathlib.RingTheory.Ideal.Over
  {A : Type u_3} {B : Type u_4} [CommRing A] [CommRing B] [Algebra A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] (G : Type u_6) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] : Subgroup.map (MulAction.stabilizer G P).subtype (Ideal.Quotient.stabilizerHom P p G).ker = Ideal.inertia G P
• IsPGroup.comap_subtype 📋 Mathlib.GroupTheory.PGroup
  {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (hH : IsPGroup p ↥H) {K : Subgroup G} : IsPGroup p ↥(Subgroup.comap K.subtype H)
• Sylow.exists_comap_subtype_eq 📋 Mathlib.GroupTheory.Sylow
  {p : ℕ} {G : Type u_1} [Group G] {H : Subgroup G} (P : Sylow p ↥H) : ∃ Q, Subgroup.comap H.subtype ↑Q = ↑P
• Sylow.normalizer_sup_eq_top 📋 Mathlib.GroupTheory.Sylow
  {G : Type u_1} [Group G] {p : ℕ} [Fact (Nat.Prime p)] {N : Subgroup G} [N.Normal] [Finite (Sylow p ↥N)] (P : Sylow p ↥N) : Subgroup.normalizer ↑(Subgroup.map N.subtype ↑P) ⊔ N = ⊤
• Sylow.card_quotient_normalizer_modEq_card_quotient 📋 Mathlib.GroupTheory.Sylow
  {G : Type u} [Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)] {H : Subgroup G} (hH : Nat.card ↥H = p ^ n) : Nat.card (↥(Subgroup.normalizer ↑H) ⧸ Subgroup.comap (Subgroup.normalizer ↑H).subtype H) ≡ Nat.card (G ⧸ H) [MOD p]
• Sylow.prime_dvd_card_quotient_normalizer 📋 Mathlib.GroupTheory.Sylow
  {G : Type u} [Group G] [Finite G] {p n : ℕ} [Fact (Nat.Prime p)] (hdvd : p ^ (n + 1) ∣ Nat.card G) {H : Subgroup G} (hH : Nat.card ↥H = p ^ n) : p ∣ Nat.card (↥(Subgroup.normalizer ↑H) ⧸ Subgroup.comap (Subgroup.normalizer ↑H).subtype H)
• Sylow.fixedPointsMulLeftCosetsEquivQuotient 📋 Mathlib.GroupTheory.Sylow
  {G : Type u} [Group G] (H : Subgroup G) [Finite ↑↑H] : ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≃ ↥(Subgroup.normalizer ↑H) ⧸ Subgroup.comap (Subgroup.normalizer ↑H).subtype H
• MonoidWithZeroHom.ValueGroup₀.embedding_apply 📋 Mathlib.Algebra.GroupWithZero.Range
  {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [GroupWithZero B] {f : A →*₀ B} (a✝ : f.ValueGroup₀) : MonoidWithZeroHom.ValueGroup₀.embedding a✝ = WithZero.recZeroCoe 0 Units.val ((WithZero.map' f.valueGroup.subtype) a✝)
• Representation.ofQuotient 📋 Mathlib.RepresentationTheory.Basic
  {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp ρ S.subtype)] : Representation k (G ⧸ S) V
• Representation.apply_eq_of_coe_eq 📋 Mathlib.RepresentationTheory.Basic
  {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [Representation.IsTrivial (MonoidHom.comp ρ S.subtype)] (g h : G) (hgh : ↑g = ↑h) : ρ g = ρ h
• Representation.ofQuotient_coe_apply 📋 Mathlib.RepresentationTheory.Basic
  {k : Type u_1} {G : Type u_2} {V : Type u_3} [Semiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp ρ S.subtype)] (g : G) (x : V) : ((ρ.ofQuotient S) ↑g) x = (ρ g) x
• ValuationSubring.ker_unitGroupToResidueFieldUnits 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) : A.unitGroupToResidueFieldUnits.ker = Subgroup.comap A.unitGroup.subtype A.principalUnitGroup
• ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) : ↥A.unitGroup ⧸ Subgroup.comap A.unitGroup.subtype A.principalUnitGroup ≃* (IsLocalRing.ResidueField ↥A)ˣ
• ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) (x : ↥A.unitGroup) : A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom ↑x = A.unitGroupToResidueFieldUnits x
• ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk 📋 Mathlib.RingTheory.Valuation.ValuationSubring
  {K : Type u} [Field K] (A : ValuationSubring K) : (↑A.unitsModPrincipalUnitsEquivResidueFieldUnits).comp (QuotientGroup.mk' (A.principalUnitGroup.subgroupOf A.unitGroup)) = A.unitGroupToResidueFieldUnits
• DiscreteTiling.PlacedTile.mk 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} (index : ιₚ) (groupElts : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps index)).subtype (↑ps index).symmetries) : DiscreteTiling.PlacedTile ps
• DiscreteTiling.PlacedTile.induction_on 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} {ppt : DiscreteTiling.PlacedTile ps → Prop} (pt : DiscreteTiling.PlacedTile ps) (h : ∀ (i : ιₚ) (gx : G), ppt { index := i, groupElts := ↑gx }) : ppt pt
• DiscreteTiling.PlacedTile.coe_mk_finite_iff 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} {i : ιₚ} (g : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i)).subtype (↑ps i).symmetries) : (↑{ index := i, groupElts := g }).Finite ↔ (↑(↑ps i)).Finite
• DiscreteTiling.PlacedTile.coe_mk_nonempty_iff 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} {i : ιₚ} (g : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i)).subtype (↑ps i).symmetries) : (↑{ index := i, groupElts := g }).Nonempty ↔ (↑(↑ps i)).Nonempty
• DiscreteTiling.PlacedTile.groupElts 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} (self : DiscreteTiling.PlacedTile ps) : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps self.index)).subtype (↑ps self.index).symmetries
• DiscreteTiling.PlacedTile.coe_mk_coe 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} (i : ιₚ) (g : G) : ↑{ index := i, groupElts := ↑g } = g • ↑(↑ps i)
• DiscreteTiling.PlacedTile.coe_mk_mk 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} (i : ιₚ) (g : G) : ↑{ index := i, groupElts := ⟦g⟧ } = g • ↑(↑ps i)
• DiscreteTiling.PlacedTile.smul_mk_coe 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} (g h : G) (i : ιₚ) : g • { index := i, groupElts := ↑h } = { index := i, groupElts := ↑(g * h) }
• DiscreteTiling.PlacedTile.smul_mk_mk 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} (g h : G) (i : ιₚ) : g • { index := i, groupElts := ⟦h⟧ } = { index := i, groupElts := ↑(g * h) }
• DiscreteTiling.PlacedTile.ext 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst✝ : Group G} {inst✝¹ : MulAction G X} {ps : DiscreteTiling.Protoset G X ιₚ} {x y : DiscreteTiling.PlacedTile ps} (index : x.index = y.index) (groupElts : x.groupElts ≍ y.groupElts) : x = y
• DiscreteTiling.PlacedTile.ext_iff 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst✝ : Group G} {inst✝¹ : MulAction G X} {ps : DiscreteTiling.Protoset G X ιₚ} {x y : DiscreteTiling.PlacedTile ps} : x = y ↔ x.index = y.index ∧ x.groupElts ≍ y.groupElts
• DiscreteTiling.PlacedTile.ext_iff_of_exists 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} {pt₁ pt₂ : DiscreteTiling.PlacedTile ps} : pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ ∃ g, ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
• DiscreteTiling.PlacedTile.ext_iff_of_preimage 📋 Mathlib.Combinatorics.Tiling.Tile
  {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [Group G] [MulAction G X] {ps : DiscreteTiling.Protoset G X ιₚ} {pt₁ pt₂ : DiscreteTiling.PlacedTile ps} : pt₁ = pt₂ ↔ pt₁.index = pt₂.index ∧ Quotient.mk (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹' {pt₁.groupElts} = Quotient.mk (QuotientGroup.leftRel (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹' {pt₂.groupElts}
• Subgroup.map_focalSubgroupOf 📋 Mathlib.GroupTheory.Focal
  {G : Type u_1} [Group G] (H : Subgroup G) : Subgroup.map H.subtype H.focalSubgroupOf = H.focalSubgroup
• Subgroup.top_subtype_lowerCentralSeries 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : Subgroup.map H.subtype (⊤.lowerCentralSeries n) = H.lowerCentralSeries n
• lowerCentralSeries_map_subtype_le 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : Subgroup.map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
• Subgroup.lowerCentralSeries_map_subtype_le 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : Subgroup.map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
• Subgroup.normal_goursatFst 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) : I.goursatFst.Normal
• Subgroup.normal_goursatSnd 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) : I.goursatSnd.Normal
• Subgroup.mk_goursatFst_eq_iff_mk_goursatSnd_eq 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) {x y : G × H} (hx : x ∈ I) (hy : y ∈ I) : ↑x.1 = ↑y.1 ↔ ↑x.2 = ↑y.2
• Subgroup.goursat_surjective 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} (hI₁ : Function.Surjective (Prod.fst ∘ ⇑I.subtype)) (hI₂ : Function.Surjective (Prod.snd ∘ ⇑I.subtype)) : have this := ⋯; have this_1 := ⋯; ∃ e, (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range = e.toMonoidHom.graph
• Subgroup.goursat 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] {I : Subgroup (G × H)} : ∃ G' H' M N, ∃ (x : M.Normal) (x_1 : N.Normal), ∃ e, I = Subgroup.map (G'.subtype.prodMap H'.subtype) (Subgroup.comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
• alternatingGroup.ofSubtype_comp_subtype 📋 Mathlib.GroupTheory.SpecificGroups.Alternating
  {α : Type u_1} [Fintype α] [DecidableEq α] (s : Finset α) : (alternatingGroup α).subtype.comp (alternatingGroup.ofSubtype s) = Equiv.Perm.ofSubtype.comp (alternatingGroup ↥s).subtype
• SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective 📋 Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
  {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] : Function.Surjective ⇑(fixingSubgroup M ∅).subtype
• SubMulAction.ofFixingSubgroup_equivariantMap 📋 Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
  (M : Type u_1) {α : Type u_2} [Group M] [MulAction M α] (s : Set α) : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[⇑(fixingSubgroup M s).subtype] α
• SubMulAction.fixingSubgroup_of_insert 📋 Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
  {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] (a : α) (s : Set ↥(SubMulAction.ofStabilizer M a)) : fixingSubgroup M (insert a ((fun x => ↑x) '' s)) = Subgroup.map (MulAction.stabilizer M a).subtype (fixingSubgroup (↥(MulAction.stabilizer M a)) s)
• SubMulAction.ofFixingSubgroup_equivariantMap_injective 📋 Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
  {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {s : Set α} : Function.Injective ⇑(SubMulAction.ofFixingSubgroup_equivariantMap M s)
• SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective 📋 Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
  {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] : Function.Bijective ⇑(SubMulAction.ofFixingSubgroup_equivariantMap M ∅)
• Subgroup.IsSubnormal.trans' 📋 Mathlib.GroupTheory.IsSubnormal
  {G : Type u_1} [Group G] {K : Subgroup G} {H : Subgroup ↥K} (Hsn : H.IsSubnormal) (Ksn : K.IsSubnormal) : (Subgroup.map K.subtype H).IsSubnormal
• Equiv.Perm.OnCycleFactors.kerParam_range_eq 📋 Mathlib.GroupTheory.Perm.Centralizer
  {α : Type u_1} [DecidableEq α] [Fintype α] {g : Equiv.Perm α} : (Equiv.Perm.OnCycleFactors.kerParam g).range = Subgroup.map (Subgroup.centralizer {g}).subtype (Equiv.Perm.OnCycleFactors.toPermHom g).ker
• TopologicalGroup.IsSES.ofClosedSubgroup 📋 Mathlib.Topology.Algebra.Group.Extension
  {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) [H.Normal] (hH : IsClosed ↑H) : TopologicalGroup.IsSES H.subtype (QuotientGroup.mk' H)
• Rep.ofQuotient 📋 Mathlib.RepresentationTheory.Rep.Res
  {k : Type u} [Semiring k] {G : Type v} [Group G] (A : Rep.{u_1, u, v} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : Rep.{u_1, u, v} k (G ⧸ S)
• Rep.resOfQuotientIso 📋 Mathlib.RepresentationTheory.Rep.Res
  {k : Type u} [Semiring k] {G : Type v} [Group G] (A : Rep.{u_1, u, v} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : Rep.res (QuotientGroup.mk' S) (A.ofQuotient S) ≅ A
• Representation.le_comap_invariants 📋 Mathlib.RepresentationTheory.Invariants
  {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_5} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] (g : G) : Representation.invariants (MonoidHom.comp ρ S.subtype) ≤ Submodule.comap (ρ g) (Representation.invariants (MonoidHom.comp ρ S.subtype))
• Representation.toInvariants 📋 Mathlib.RepresentationTheory.Invariants
  {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_5} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k G ↥(Representation.invariants (MonoidHom.comp ρ S.subtype))
• Representation.quotientToInvariants 📋 Mathlib.RepresentationTheory.Invariants
  {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_5} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k (G ⧸ S) ↥(Representation.invariants (MonoidHom.comp ρ S.subtype))
• Representation.quotientToInvariants_lift 📋 Mathlib.RepresentationTheory.Invariants
  {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_5} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation.IntertwiningMap (MonoidHom.comp (ρ.quotientToInvariants S) (QuotientGroup.mk' S)) ρ
• Representation.instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants 📋 Mathlib.RepresentationTheory.Invariants
  {k : Type u_1} {G : Type u_2} [CommRing k] [Group G] {V : Type u_5} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation.IsTrivial (MonoidHom.comp (ρ.toInvariants S) S.subtype)
• Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype 📋 Mathlib.RepresentationTheory.Coinduced
  {k : Type u} [CommRing k] {G : Type v'} [Group G] (S : Subgroup G) : (Rep.coindFunctor k S.subtype).PreservesEpimorphisms
• Rep.instPreservesProjectiveObjectsSubtypeMemSubgroupResFunctorSubtype 📋 Mathlib.RepresentationTheory.Coinduced
  {k : Type u} [CommRing k] {G : Type w} [Group G] (S : Subgroup G) : (Rep.resFunctor S.subtype).PreservesProjectiveObjects
• Representation.Coinvariants.le_comap_ker 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] (g : G) : Representation.Coinvariants.ker (MonoidHom.comp ρ S.subtype) ≤ Submodule.comap (ρ g) (Representation.Coinvariants.ker (MonoidHom.comp ρ S.subtype))
• Rep.quotientToCoinvariantsFunctor_obj_V 📋 Mathlib.RepresentationTheory.Coinvariants
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] (X : Rep.{w, u, v} k G) : ↑((Rep.quotientToCoinvariantsFunctor k S).obj X) = Representation.Coinvariants (MonoidHom.comp X.ρ S.subtype)
• Representation.toCoinvariantsKer 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k G ↥(Representation.Coinvariants.ker (MonoidHom.comp ρ S.subtype))
• Representation.toCoinvariants 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k G (Representation.Coinvariants (MonoidHom.comp ρ S.subtype))
• Representation.toCoinvariantsMkQ 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : ρ.IntertwiningMap (ρ.toCoinvariants S)
• Representation.quotientToCoinvariants 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation k (G ⧸ S) (Representation.Coinvariants (MonoidHom.comp ρ S.subtype))
• Rep.coinvariantsShortComplex_f 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u} {G : Type v} [CommRing k] [Group G] (A : Rep.{w, u, v} k G) (S : Subgroup G) [S.Normal] : (A.coinvariantsShortComplex S).f = Rep.ofHom { toLinearMap := (Representation.Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ }
• Rep.quotientToCoinvariantsFunctor_map_hom_toLinearMap 📋 Mathlib.RepresentationTheory.Coinvariants
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y) : (Rep.Hom.hom ((Rep.quotientToCoinvariantsFunctor k S).map f)).toLinearMap = Representation.Coinvariants.map (MonoidHom.comp X.ρ S.subtype) (MonoidHom.comp Y.ρ S.subtype) (Rep.Hom.hom (Rep.resMap S.subtype f))
• Representation.instIsTrivialSubtypeMemSubgroupCoinvariantsCompLinearMapIdSubtypeToCoinvariants 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] : Representation.IsTrivial (MonoidHom.comp (ρ.toCoinvariants S) S.subtype)
• Representation.toCoinvariants_mk 📋 Mathlib.RepresentationTheory.Coinvariants
  {k : Type u_6} {G : Type u_7} {V : Type u_8} [CommRing k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] (g : G) (x : V) : ((ρ.toCoinvariants S) g) ((Representation.Coinvariants.mk (MonoidHom.comp ρ S.subtype)) x) = (Representation.Coinvariants.mk (MonoidHom.comp ρ S.subtype)) ((ρ g) x)
• Rep.instIsRightAdjointSubtypeMemSubgroupIndFunctorSubtype 📋 Mathlib.RepresentationTheory.FiniteIndex
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [S.FiniteIndex] : (Rep.indFunctor k S.subtype).IsRightAdjoint
• Rep.indCoindIso 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S) : Rep.ind S.subtype A ≅ Rep.coind.{u, v, v, max u w} S.subtype A
• Rep.instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [S.FiniteIndex] : (Rep.coindFunctor k S.subtype).IsLeftAdjoint
• Rep.resIndAdjunction 📋 Mathlib.RepresentationTheory.FiniteIndex
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] : Rep.resFunctor S.subtype ⊣ Rep.indFunctor k S.subtype
• Rep.coindResAdjunction 📋 Mathlib.RepresentationTheory.FiniteIndex
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] : Rep.coindFunctor k S.subtype ⊣ Rep.resFunctor S.subtype
• Rep.indCoindNatIso 📋 Mathlib.RepresentationTheory.FiniteIndex
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] : Rep.indFunctor k S.subtype ≅ Rep.coindFunctor k S.subtype
• Rep.indCoindNatIso_hom_app 📋 Mathlib.RepresentationTheory.FiniteIndex
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (X : Rep.{max u w, u, v} k ↥S) : (Rep.indCoindNatIso k S).hom.app X = X.indCoindIso.hom
• Rep.indCoindNatIso_inv_app 📋 Mathlib.RepresentationTheory.FiniteIndex
  (k : Type u) {G : Type v} [CommRing k] [Group G] (S : Subgroup G) [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (X : Rep.{max u w, u, v} k ↥S) : (Rep.indCoindNatIso k S).inv.app X = X.indCoindIso.inv
• Rep.coindResAdjunction_counit_app 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (B : Rep.{max w u v, u, v} k G) : (Rep.coindResAdjunction k S).counit.app B = CategoryTheory.CategoryStruct.comp (Rep.res S.subtype B).indCoindIso.inv ((Rep.indResAdjunction k S.subtype).counit.app B)
• Rep.resIndAdjunction_unit_app 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (B : Rep.{max w u v, u, v} k G) : (Rep.resIndAdjunction k S).unit.app B = CategoryTheory.CategoryStruct.comp ((Rep.resCoindAdjunction k S.subtype).unit.app B) (Rep.res S.subtype B).indCoindIso.inv
• Rep.resIndAdjunction_counit_app 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S) : (Rep.resIndAdjunction k S).counit.app A = CategoryTheory.CategoryStruct.comp ((Rep.resFunctor S.subtype).map A.indCoindIso.hom) ((Rep.resCoindAdjunction k S.subtype).counit.app A)
• Rep.coindResAdjunction_unit_app 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S) : (Rep.coindResAdjunction k S).unit.app A = CategoryTheory.CategoryStruct.comp ((Rep.indResAdjunction k S.subtype).unit.app A) ((Rep.resFunctor S.subtype).map A.indCoindIso.hom)
• Rep.coindToInd 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] : ↑(Rep.coind.{u, v, v, w} S.subtype A) →ₗ[k] ↑(Rep.ind S.subtype A)
• Rep.indToCoind 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) : ↑(Rep.ind S.subtype A) →ₗ[k] ↑(Rep.coind.{u, v, v, w} S.subtype A)
• Rep.coindResAdjunction_homEquiv_apply 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S) {B : Rep.{max (max u v) w, u, v} k G} (f : Rep.coind.{u, v, v, max (max u v) w} S.subtype A ⟶ B) : ((Rep.coindResAdjunction k S).homEquiv A B) f = (Rep.indResHomEquiv S.subtype A B) (CategoryTheory.CategoryStruct.comp A.indCoindIso.hom f)
• Rep.resIndAdjunction_homEquiv_apply 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S) {B : Rep.{max w u v, u, v} k G} (f : Rep.res S.subtype B ⟶ A) : ((Rep.resIndAdjunction k S).homEquiv B A) f = CategoryTheory.CategoryStruct.comp ((Rep.resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A) f) A.indCoindIso.inv
• Rep.coindResAdjunction_homEquiv_symm_apply 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S) {B : Rep.{max (max u v) w, u, v} k G} (f : A ⟶ Rep.res S.subtype B) : ((Rep.coindResAdjunction k S).homEquiv A B).symm f = CategoryTheory.CategoryStruct.comp A.indCoindIso.inv ((Rep.indResHomEquiv S.subtype A B).symm f)
• Rep.resIndAdjunction_homEquiv_symm_apply 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S) {B : Rep.{max w u v, u, v} k G} (f : B ⟶ (Rep.indFunctor k S.subtype).obj A) : ((Rep.resIndAdjunction k S).homEquiv B A).symm f = (Rep.resCoindHomEquiv.{max w u v, u, v, v} S.subtype B A).symm (CategoryTheory.CategoryStruct.comp f A.indCoindIso.hom)
• Rep.coindToInd_indToCoind 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] : A.indToCoind ∘ₗ A.coindToInd = LinearMap.id
• Rep.indToCoind_coindToInd 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] : A.coindToInd ∘ₗ A.indToCoind = LinearMap.id
• Rep.coindToInd_apply 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} (A : Rep.{w, u, v} k ↥S) [S.FiniteIndex] (f : ↑(Rep.coind.{u, v, v, w} S.subtype A)) : A.coindToInd f = ∑ g, g.liftOn (fun g => (Representation.IndV.mk S.subtype A.ρ g) (↑f g)) ⋯
• Rep.coindToInd_of_support_subset_orbit 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} {A : Rep.{w, u, v} k ↥S} [S.FiniteIndex] (g : G) (f : ↑(Rep.coind.{u, v, v, w} S.subtype A)) (hx : Function.support ↑f ⊆ MulAction.orbit (↥S) g) : A.coindToInd f = (Representation.IndV.mk S.subtype A.ρ g) (↑f g)
• Rep.indCoindIso_hom_hom_toLinearMap 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S) : (Rep.Hom.hom A.indCoindIso.hom).toLinearMap = A.indToCoind
• Rep.indCoindIso_inv_hom_toLinearMap 📋 Mathlib.RepresentationTheory.FiniteIndex
  {k : Type u} {G : Type v} [CommRing k] [Group G] {S : Subgroup G} [DecidableRel ⇑(QuotientGroup.rightRel S)] [S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S) : (Rep.Hom.hom A.indCoindIso.inv).toLinearMap = { toFun := (Representation.Equiv.mk (LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ⋯).invFun, map_add' := ⋯, map_smul' := ⋯ }
• groupCohomology.H1InfRes_X₃ 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] : (groupCohomology.H1InfRes A S).X₃ = groupCohomology (Rep.res S.subtype A) 1
• groupCohomology.H1InfRes_g 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] : (groupCohomology.H1InfRes A S).g = groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) 1
• groupCohomology.coindIso 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (A : Rep.{u, u, u} k ↥S) (n : ℕ) : groupCohomology (Rep.coind.{u, u, u, u} S.subtype A) n ≅ groupCohomology A n
• groupCohomology.linearYonedaObjResProjectiveResolutionIso 📋 Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
  {k G : Type u} [CommRing k] [Group G] {S : Subgroup G} (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) (A : Rep.{u, u, u} k ↥S) : ((Rep.resFunctor S.subtype).mapProjectiveResolution P).complex.linearYonedaObj k A ≅ P.complex.linearYonedaObj k (Rep.coind.{u, u, u, u} S.subtype A)
• groupHomology.H1CoresCoinf_X₁ 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] : (groupHomology.H1CoresCoinf A S).X₁ = groupHomology.H1 (Rep.res S.subtype A)
• groupHomology.H1CoresCoinf_f 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] : (groupHomology.H1CoresCoinf A S).f = groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) 1
• groupHomology.H1CoresCoinfOfTrivial 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.ShortComplex (ModuleCat k)
• groupHomology.H1CoresCoinfOfTrivial_exact 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (groupHomology.H1CoresCoinfOfTrivial A S).Exact
• groupHomology.H1CoresCoinfOfTrivial_X₂ 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (groupHomology.H1CoresCoinfOfTrivial A S).X₂ = groupHomology.H1 A
• groupHomology.H1CoresCoinfOfTrivial_X₃ 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (groupHomology.H1CoresCoinfOfTrivial A S).X₃ = groupHomology.H1 (A.ofQuotient S)
• groupHomology.H1CoresCoinfOfTrivial_g_epi 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.Epi (groupHomology.H1CoresCoinfOfTrivial A S).g
• groupHomology.H1CoresCoinfOfTrivial_X₁ 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (groupHomology.H1CoresCoinfOfTrivial A S).X₁ = groupHomology.H1 (Rep.res S.subtype A)
• groupHomology.map₁_quotientGroupMk'_epi 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.Epi (groupHomology.map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1)
• groupHomology.H1CoresCoinfOfTrivial_g 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (groupHomology.H1CoresCoinfOfTrivial A S).g = groupHomology.map (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv 1
• groupHomology.H1CoresCoinfOfTrivial_f 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : (groupHomology.H1CoresCoinfOfTrivial A S).f = groupHomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A)) 1
• groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] : Submodule.comap (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (groupHomology.mapShortComplexH1 (MonoidHom.id G) (A.coinvariantsShortComplex S).f).τ₂ (groupHomology.shortComplexH1 A).pOpcycles)) (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp (groupHomology.mapShortComplexH1 S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype A))).τ₂ (groupHomology.shortComplexH1 A).pOpcycles)).range = ⊤
• groupHomology.mapCycles₁_quotientGroupMk'_epi 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
  {k G : Type u} [CommRing k] [Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [S.Normal] [Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)] : CategoryTheory.Epi (groupHomology.mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)
• groupHomology.indIso 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro
  {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [DecidableEq G] (A : Rep.{u, u, u} k ↥S) (n : ℕ) : groupHomology (Rep.ind S.subtype A) n ≅ groupHomology A n
• groupHomology.coinvariantsTensorResProjectiveResolutionIso 📋 Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro
  {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) (A : Rep.{u, u, u} k ↥S) (P : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)) : HomologicalComplex.coinvariantsTensorObj A ((Rep.resFunctor S.subtype).mapProjectiveResolution P).complex ≅ HomologicalComplex.coinvariantsTensorObj (Rep.ind S.subtype A) P.complex

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59