Loogle!

Result

Found 109 declarations mentioning Group, HasQuotient.Quotient and Subgroup.Normal.

QuotientGroup.Quotient.group 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Group (G ⧸ N)
QuotientGroup.Quotient.group.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : QuotientGroup.Quotient.group N = (QuotientGroup.con N).group
QuotientGroup.eq_iff_div_mem 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {x y : G} : ↑x = ↑y ↔ x / y ∈ N
QuotientGroup.mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : G →* G ⧸ N
QuotientGroup.ker_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : (QuotientGroup.mk' N).ker = N
QuotientGroup.preimage_image_coe 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (s : Set G) : QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' s) = ↑N * s
QuotientGroup.range_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : (QuotientGroup.mk' N).range = ⊤
QuotientGroup.map_mk'_self 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Subgroup.map (QuotientGroup.mk' N) N = ⊥
QuotientGroup.Quotient.commGroup.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u_1} [CommGroup G] (N : Subgroup G) : QuotientGroup.Quotient.commGroup N = { toGroup := let_fun this := ⋯; QuotientGroup.Quotient.group N, mul_comm := ⋯ }
QuotientGroup.mk_inv 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) : ↑a⁻¹ = (↑a)⁻¹
QuotientGroup.mk'.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : QuotientGroup.mk' N = MonoidHom.mk' QuotientGroup.mk ⋯
QuotientGroup.mk_zpow 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ℤ) : ↑(a ^ n) = ↑a ^ n
QuotientGroup.mk_one 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : ↑1 = 1
QuotientGroup.lift 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N ≤ φ.ker) : G ⧸ N →* M
QuotientGroup.eq_one_iff 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {N : Subgroup G} [N.Normal] (x : G) : ↑x = 1 ↔ x ∈ N
QuotientGroup.mk_div 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a b : G) : ↑(a / b) = ↑a / ↑b
QuotientGroup.mk_pow 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a : G) (n : ℕ) : ↑(a ^ n) = ↑a ^ n
QuotientGroup.image_coe 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : QuotientGroup.mk '' ↑N = 1
QuotientGroup.image_coe_inj 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {s t : Set G} : QuotientGroup.mk '' s = QuotientGroup.mk '' t ↔ ↑N * s = ↑N * t
QuotientGroup.ker_lift 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N ≤ φ.ker) : (QuotientGroup.lift N φ HN).ker = Subgroup.map (QuotientGroup.mk' N) φ.ker
QuotientGroup.mk_mul 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (a b : G) : ↑(a * b) = ↑a * ↑b
QuotientGroup.lift_comp_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N ≤ φ.ker) : (QuotientGroup.lift N φ HN).comp (QuotientGroup.mk' N) = φ
QuotientGroup.mk'_surjective 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : Function.Surjective ⇑(QuotientGroup.mk' N)
QuotientGroup.lift.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (HN : N ≤ φ.ker) : QuotientGroup.lift N φ HN = (QuotientGroup.con N).lift φ ⋯
QuotientGroup.coe_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] : ⇑(QuotientGroup.mk' N) = QuotientGroup.mk
QuotientGroup.mk'_apply 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (x : G) : (QuotientGroup.mk' N) x = ↑x
QuotientGroup.map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) : G ⧸ N →* H ⧸ M
QuotientGroup.ker_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) : (QuotientGroup.map N M f h).ker = Subgroup.map (QuotientGroup.mk' N) (Subgroup.comap f M)
QuotientGroup.lift_mk 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : (QuotientGroup.lift N φ HN) ↑g = φ g
QuotientGroup.lift_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : (QuotientGroup.lift N φ HN) ↑g = φ g
QuotientGroup.lift_quot_mk 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] {φ : G →* M} (HN : N ≤ φ.ker) (g : G) : (QuotientGroup.lift N φ HN) (Quot.mk (⇑(QuotientGroup.leftRel N)) g) = φ g
QuotientGroup.lift_surjective_of_surjective 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] (φ : G →* M) (hφ : Function.Surjective ⇑φ) (HN : N ≤ φ.ker) : Function.Surjective ⇑(QuotientGroup.lift N φ HN)
QuotientGroup.map_id 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : N ≤ Subgroup.comap (MonoidHom.id G) N := ⋯) : QuotientGroup.map N N (MonoidHom.id G) h = MonoidHom.id (G ⧸ N)
QuotientGroup.map.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) : QuotientGroup.map N M f h = QuotientGroup.lift N ((QuotientGroup.mk' M).comp f) ⋯
QuotientGroup.monoidHom_ext 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {M : Type x} [Monoid M] ⦃f g : G ⧸ N →* M⦄ (h : f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)) : f = g
QuotientGroup.monoidHom_ext_iff 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {N : Subgroup G} [nN : N.Normal] {M : Type x} [Monoid M] {f g : G ⧸ N →* M} : f = g ↔ f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N)
QuotientGroup.mk'_eq_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {x y : G} : (QuotientGroup.mk' N) x = (QuotientGroup.mk' N) y ↔ ∃ z ∈ N, x * z = y
QuotientGroup.congr 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : G ⧸ G' ≃* H ⧸ H'
QuotientGroup.map_id_apply 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (h : N ≤ Subgroup.comap (MonoidHom.id G) N := ⋯) (x : G ⧸ N) : (QuotientGroup.map N N (MonoidHom.id G) h) x = x
QuotientGroup.map_mk 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) (x : G) : (QuotientGroup.map N M f h) ↑x = ↑(f x)
QuotientGroup.map_surjective_of_surjective 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (hf : Function.Surjective (QuotientGroup.mk ∘ ⇑f)) (h : N ≤ Subgroup.comap f M) : Function.Surjective ⇑(QuotientGroup.map N M f h)
QuotientGroup.congr_refl 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (G' : Subgroup G) [G'.Normal] (he : Subgroup.map (↑(MulEquiv.refl G)) G' = G' := ⋯) : QuotientGroup.congr G' G' (MulEquiv.refl G) he = MulEquiv.refl (G ⧸ G')
QuotientGroup.map_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ Subgroup.comap f M) (x : G) : (QuotientGroup.map N M f h) ((QuotientGroup.mk' N) x) = ↑(f x)
QuotientGroup.map_comp_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : N ≤ Subgroup.comap (g.comp f) O := ⋯) : (QuotientGroup.map M O g hg).comp (QuotientGroup.map N M f hf) = QuotientGroup.map N O (g.comp f) hgf
QuotientGroup.congr_mk 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : (QuotientGroup.congr G' H' e he) ↑x = ↑(e x)
QuotientGroup.congr_apply 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : (QuotientGroup.congr G' H' e he) ↑x = (QuotientGroup.mk' H') (e x)
QuotientGroup.congr_symm 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : (QuotientGroup.congr G' H' e he).symm = QuotientGroup.congr H' G' e.symm ⋯
QuotientGroup.congr_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') (x : G) : (QuotientGroup.congr G' H' e he) ((QuotientGroup.mk' G') x) = (QuotientGroup.mk' H') (e x)
QuotientGroup.ker_le_range_iff 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {H : Type v} [Group H] {I : Type w} [MulOneClass I] (f : G →* H) [f.range.Normal] (g : H →* I) : g.ker ≤ f.range ↔ (QuotientGroup.mk' f.range).comp g.ker.subtype = 1
QuotientGroup.map_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] {H : Type v} [Group H] {I : Type u_1} [Group I] (M : Subgroup H) (O : Subgroup I) [M.Normal] [O.Normal] (f : G →* H) (g : H →* I) (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : N ≤ Subgroup.comap (g.comp f) O := ⋯) (x : G ⧸ N) : (QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (g.comp f) hgf) x
QuotientGroup.congr.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [Group G] {H : Type v} [Group H] (G' : Subgroup G) (H' : Subgroup H) [G'.Normal] [H'.Normal] (e : G ≃* H) (he : Subgroup.map (↑e) G' = H') : QuotientGroup.congr G' H' e he = { toFun := ⇑(QuotientGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
QuotientGroup.map_normal 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] : (Subgroup.map (QuotientGroup.mk' N) M).Normal
QuotientGroup.le_comap_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [N.Normal] (H : Subgroup (G ⧸ N)) : N ≤ Subgroup.comap (QuotientGroup.mk' N) H
QuotientGroup.comap_map_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N H : Subgroup G) [N.Normal] : Subgroup.comap (QuotientGroup.mk' N) (Subgroup.map (QuotientGroup.mk' N) H) = N ⊔ H
QuotientGroup.quotientMulEquivOfEq 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N
QuotientGroup.comapMk'OrderIso 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [hn : N.Normal] : Subgroup (G ⧸ N) ≃o { H // N ≤ H }
QuotientGroup.quotientMulEquivOfEq.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) : QuotientGroup.quotientMulEquivOfEq h = { toEquiv := Subgroup.quotientEquivOfEq h, map_mul' := ⋯ }
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)
QuotientGroup.quotientQuotientEquivQuotientAux 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M →* G ⧸ M
QuotientGroup.quotientMulEquivOfEq_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {M N : Subgroup G} [M.Normal] [N.Normal] (h : M = N) (x : G) : (QuotientGroup.quotientMulEquivOfEq h) ↑x = ↑x
QuotientGroup.comap_comap_center 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {H₁ : Subgroup G} [H₁.Normal] {H₂ : Subgroup (G ⧸ H₁)} [H₂.Normal] : Subgroup.comap (QuotientGroup.mk' H₁) (Subgroup.comap (QuotientGroup.mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) = Subgroup.comap (QuotientGroup.mk' (Subgroup.comap (QuotientGroup.mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (QuotientGroup.mk' H₁) H₂))
QuotientGroup.sound 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (U : Set (G ⧸ N)) (g : ↥N.op) : g • ⇑(QuotientGroup.mk' N) ⁻¹' U = ⇑(QuotientGroup.mk' N) ⁻¹' U
QuotientGroup.quotientQuotientEquivQuotient 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ Subgroup.map (QuotientGroup.mk' N) M ≃* G ⧸ M
QuotientGroup.quotientQuotientEquivQuotientAux.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : QuotientGroup.quotientQuotientEquivQuotientAux N M h = QuotientGroup.lift (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.map N M (MonoidHom.id G) h) ⋯
QuotientGroup.comapMk'OrderIso.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [hn : N.Normal] : QuotientGroup.comapMk'OrderIso N = { toFun := fun H' => ⟨Subgroup.comap (QuotientGroup.mk' N) H', ⋯⟩, invFun := fun H => Subgroup.map (QuotientGroup.mk' N) ↑H, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
QuotientGroup.quotientMapSubgroupOfOfLe 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) : ↥A ⧸ A'.subgroupOf A →* ↥B ⧸ B'.subgroupOf B
QuotientGroup.quotientMapSubgroupOfOfLe.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) : QuotientGroup.quotientMapSubgroupOfOfLe h' h = QuotientGroup.map (A'.subgroupOf A) (B'.subgroupOf B) (Subgroup.inclusion h) ⋯
QuotientGroup.equivQuotientSubgroupOfOfEq 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal] [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) : ↥A ⧸ A'.subgroupOf A ≃* ↥B ⧸ B'.subgroupOf B
QuotientGroup.quotientQuotientEquivQuotient.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) : QuotientGroup.quotientQuotientEquivQuotient N M h = (QuotientGroup.quotientQuotientEquivQuotientAux N M h).toMulEquiv (QuotientGroup.map M (Subgroup.map (QuotientGroup.mk' N) M) (QuotientGroup.mk' N) ⋯) ⋯ ⋯
QuotientGroup.quotientQuotientEquivQuotientAux_mk_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
QuotientGroup.quotientQuotientEquivQuotientAux_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (N : Subgroup G) [nN : N.Normal] (M : Subgroup G) [nM : M.Normal] (h : N ≤ M) (x : G ⧸ N) : (QuotientGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientGroup.map N M (MonoidHom.id G) h) x
QuotientGroup.equivQuotientSubgroupOfOfEq.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {A' A B' B : Subgroup G} [hAN : (A'.subgroupOf A).Normal] [hBN : (B'.subgroupOf B).Normal] (h' : A' = B') (h : A = B) : QuotientGroup.equivQuotientSubgroupOfOfEq h' h = (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯).toMulEquiv (QuotientGroup.quotientMapSubgroupOfOfLe ⋯ ⋯) ⋯ ⋯
QuotientGroup.quotientInfEquivProdNormalQuotient 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (H N : Subgroup G) [hN : N.Normal] : ↥H ⧸ N.subgroupOf H ≃* ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)
QuotientGroup.quotientInfEquivProdNormalQuotient.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] (H N : Subgroup G) [hN : N.Normal] : QuotientGroup.quotientInfEquivProdNormalQuotient H N = QuotientGroup.quotientInfEquivProdNormalizerQuotient H N ⋯
QuotientGroup.quotientMapSubgroupOfOfLe_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [Group G] {A' A B' B : Subgroup G} [_hAN : (A'.subgroupOf A).Normal] [_hBN : (B'.subgroupOf B).Normal] (h' : A' ≤ B') (h : A ≤ B) (x : ↥A) : (QuotientGroup.quotientMapSubgroupOfOfLe h' h) ↑x = ↑((Subgroup.inclusion h) x)
Group.fintypeOfDomOfCoker 📋 Mathlib.GroupTheory.QuotientGroup.Finite
{F G : Type u} [Group F] [Group G] [Fintype F] (f : F →* G) [f.range.Normal] [Fintype (G ⧸ f.range)] : Fintype G
Group.fintypeOfDomOfCoker.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Finite
{F G : Type u} [Group F] [Group G] [Fintype F] (f : F →* G) [f.range.Normal] [Fintype (G ⧸ f.range)] : Group.fintypeOfDomOfCoker f = Group.fintypeOfKerLeRange f (QuotientGroup.mk' f.range) ⋯
QuotientGroup.fg 📋 Mathlib.GroupTheory.Finiteness
{G : Type u_3} [Group G] [Group.FG G] (N : Subgroup G) [N.Normal] : Group.FG (G ⧸ N)
Subgroup.Normal.quotient_commutative_iff_commutator_le 📋 Mathlib.GroupTheory.Abelianization
{G : Type u} [Group G] {N : Subgroup G} [N.Normal] : (Std.Commutative fun x1 x2 => x1 * x2) ↔ commutator G ≤ N
QuotientGroup.instIsTopologicalGroup 📋 Mathlib.Topology.Algebra.Group.Quotient
{G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] : IsTopologicalGroup (G ⧸ N)
QuotientGroup.instT3Space 📋 Mathlib.Topology.Algebra.Group.Quotient
{G : Type u_1} [TopologicalSpace G] [Group G] [IsTopologicalGroup G] (N : Subgroup G) [N.Normal] [hN : IsClosed ↑N] : T3Space (G ⧸ N)
QuotientGroup.completeSpace' 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [CompleteSpace G] : CompleteSpace (G ⧸ N)
QuotientGroup.completeSpace 📋 Mathlib.Topology.Algebra.IsUniformGroup.Basic
(G : Type u) [Group G] [us : UniformSpace G] [IsUniformGroup G] [FirstCountableTopology G] (N : Subgroup G) [N.Normal] [hG : CompleteSpace G] : CompleteSpace (G ⧸ N)
IsPGroup.to_quotient 📋 Mathlib.GroupTheory.PGroup
{p : ℕ} {G : Type u_1} [Group G] (hG : IsPGroup p G) (H : Subgroup G) [H.Normal] : IsPGroup p (G ⧸ H)
solvable_quotient_of_solvable 📋 Mathlib.GroupTheory.Solvable
{G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [IsSolvable G] : IsSolvable (G ⧸ H)
QuotientGroup.borelSpace 📋 Mathlib.MeasureTheory.Constructions.Polish.Basic
{G : Type u_3} [TopologicalSpace G] [PolishSpace G] [Group G] [IsTopologicalGroup G] [MeasurableSpace G] [BorelSpace G] {N : Subgroup G} [N.Normal] [IsClosed ↑N] : BorelSpace (G ⧸ N)
MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
{G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G) [ν.IsMulLeftInvariant] [hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν] [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] : μ.IsMulLeftInvariant
MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
{G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G) [ν.IsHaarMeasure] [ν.IsMulRightInvariant] [LocallyCompactSpace G] [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] [i : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν] [MeasureTheory.IsFiniteMeasure μ] : μ.IsHaarMeasure
MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
{G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G) [ν.IsMulLeftInvariant] [Countable ↥Γ] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsMulLeftInvariant] [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure μ] [hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν] (h : MeasureTheory.covolume (↥Γ.op) G ν = μ Set.univ) : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
{G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] [Countable ↥Γ] (ν : MeasureTheory.Measure G) [ν.IsHaarMeasure] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] (K : TopologicalSpace.PositiveCompacts (G ⧸ Γ)) {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν) (h𝓕_finite : ν 𝓕 ≠ ⊤) : MeasureTheory.QuotientMeasureEqMeasurePreimage ν (ν (QuotientGroup.mk ⁻¹' ↑K ∩ 𝓕) • MeasureTheory.Measure.haarMeasure K)
IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
{G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} [Countable ↥Γ] (ν : MeasureTheory.Measure G) [ν.IsHaarMeasure] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] {𝓕 : Set G} (h𝓕 : MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν) [μ.IsMulLeftInvariant] [MeasureTheory.SigmaFinite μ] {V : Set (G ⧸ Γ)} (hV : (interior V).Nonempty) (meas_V : MeasurableSet V) (hμK : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ 𝓕)) (neTopV : μ V ≠ ⊤) : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set 📋 Mathlib.MeasureTheory.Measure.Haar.Quotient
{G : Type u_1} [Group G] [MeasurableSpace G] [TopologicalSpace G] [IsTopologicalGroup G] [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [Γ.Normal] [T2Space (G ⧸ Γ)] [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G) [ν.IsMulLeftInvariant] [Countable ↥Γ] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsMulLeftInvariant] [MeasureTheory.SigmaFinite μ] {s : Set G} (fund_dom_s : MeasureTheory.IsFundamentalDomain (↥Γ.op) s ν) {V : Set (G ⧸ Γ)} (meas_V : MeasurableSet V) (neZeroV : μ V ≠ 0) (hV : μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s)) (neTopV : μ V ≠ ⊤) : MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ
Subgroup.IsComplement'.QuotientMulEquiv 📋 Mathlib.GroupTheory.Complement
{G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) : G ⧸ K ≃* ↥H
Subgroup.IsComplement'.QuotientMulEquiv_apply 📋 Mathlib.GroupTheory.Complement
{G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) (a✝ : G ⧸ K) : h.QuotientMulEquiv a✝ = (Subgroup.IsComplement.leftQuotientEquiv h) a✝
Subgroup.IsComplement'.QuotientMulEquiv_symm_apply 📋 Mathlib.GroupTheory.Complement
{G : Type u_1} [Group G] {H K : Subgroup G} [K.Normal] (h : H.IsComplement' K) (a✝ : ↥H) : h.QuotientMulEquiv.symm a✝ = (Subgroup.IsComplement.leftQuotientEquiv h).symm a✝
Action.FintypeCat.toEndHom 📋 Mathlib.CategoryTheory.Action.Concrete
{G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] : G →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
Action.FintypeCat.quotientToEndHom 📋 Mathlib.CategoryTheory.Action.Concrete
{G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] : ↥H ⧸ N.subgroupOf H →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
Action.FintypeCat.toEndHom_trivial_of_mem 📋 Mathlib.CategoryTheory.Action.Concrete
{G : Type u_1} [Group G] {N : Subgroup G} [Fintype (G ⧸ N)] [N.Normal] {n : G} (hn : n ∈ N) : (Action.FintypeCat.toEndHom N) n = CategoryTheory.CategoryStruct.id (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
Action.FintypeCat.toEndHom_apply 📋 Mathlib.CategoryTheory.Action.Concrete
{G : Type u_1} [Group G] (N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (g h : G) : ((Action.FintypeCat.toEndHom N) g).hom ⟦h⟧ = ⟦h * g⁻¹⟧
Action.FintypeCat.quotientToEndHom_mk 📋 Mathlib.CategoryTheory.Action.Concrete
{G : Type u_1} [Group G] (H N : Subgroup G) [Fintype (G ⧸ N)] [N.Normal] (x : ↥H) (g : G) : ((Action.FintypeCat.quotientToEndHom H N) ⟦x⟧).hom ⟦g⟧ = ⟦g * ↑x⁻¹⟧
Finset.le_card_quotient_mul_sq_inter_subgroup 📋 Mathlib.Geometry.Group.Growth.QuotientInter
{G : Type u_1} [Group G] [DecidableEq G] {H : Subgroup G} [DecidablePred fun x => x ∈ H] [H.Normal] {A : Finset G} (hAsymm : A⁻¹ = A) : A.card ≤ (Finset.image (⇑(QuotientGroup.mk' H)) A).card * {x ∈ A ^ 2 | x ∈ H}.card
Finset.card_pow_quotient_mul_pow_inter_subgroup_le 📋 Mathlib.Geometry.Group.Growth.QuotientInter
{G : Type u_1} [Group G] [DecidableEq G] {H : Subgroup G} [DecidablePred fun x => x ∈ H] [H.Normal] {A : Finset G} {m n : ℕ} : (Finset.image (⇑(QuotientGroup.mk' H)) (A ^ m)).card * {x ∈ A ^ n | x ∈ H}.card ≤ (A ^ (m + n)).card
Subgroup.commProb_quotient_le 📋 Mathlib.GroupTheory.CommutingProbability
{G : Type u_2} [Group G] [Finite G] (H : Subgroup G) [H.Normal] : commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)
nilpotent_quotient_of_nilpotent 📋 Mathlib.GroupTheory.Nilpotent
{G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [_h : Group.IsNilpotent G] : Group.IsNilpotent (G ⧸ H)
nilpotencyClass_quotient_le 📋 Mathlib.GroupTheory.Nilpotent
{G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] [_h : Group.IsNilpotent G] : Group.nilpotencyClass (G ⧸ H) ≤ Group.nilpotencyClass G
upperCentralSeriesStep_eq_comap_center 📋 Mathlib.GroupTheory.Nilpotent
{G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : upperCentralSeriesStep H = Subgroup.comap (QuotientGroup.mk' H) (Subgroup.center (G ⧸ H))
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)) : let_fun this := ⋯; let_fun 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)
IsZGroup.instQuotientSubgroupOfFinite 📋 Mathlib.GroupTheory.SpecificGroups.ZGroup
{G : Type u_1} [Group G] [Finite G] [IsZGroup G] (H : Subgroup G) [H.Normal] : IsZGroup (G ⧸ H)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. 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:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
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
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.

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.

This is Loogle revision 19971e9 serving mathlib revision bce1d65