Loogle!

Result

Found 171 declarations mentioning Subgroup.closure.

• Subgroup.closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (k : Set G) : Subgroup G
• Subgroup.closure_univ 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] : Subgroup.closure Set.univ = ⊤
• Subgroup.closure_empty 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] : Subgroup.closure ∅ = ⊥
• Subgroup.closure_eq 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (K : Subgroup G) : Subgroup.closure ↑K = K
• Subgroup.subset_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} : k ⊆ ↑(Subgroup.closure k)
• Subgroup.mem_closure_singleton_self 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (x : G) : x ∈ Subgroup.closure {x}
• Subgroup.mem_closure_of_mem 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {s : Set G} {x : G} (hx : x ∈ s) : x ∈ Subgroup.closure s
• Subgroup.notMem_of_notMem_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} {P : G} (hP : P ∉ Subgroup.closure k) : P ∉ k
• Subgroup.closure_insert_one 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.closure (insert 1 s) = Subgroup.closure s
• Subgroup.closure_mono 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] ⦃h k : Set G⦄ (h' : h ⊆ k) : Subgroup.closure h ≤ Subgroup.closure k
• Subgroup.closure_singleton_one 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] : Subgroup.closure {1} = ⊥
• Subgroup.closure_diff_one 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.closure (s \ {1}) = Subgroup.closure s
• Subgroup.closure_iUnion 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {ι : Sort u_2} (s : ι → Set G) : Subgroup.closure (⋃ i, s i) = ⨆ i, Subgroup.closure (s i)
• Subgroup.closure_sdiff_one 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.closure (s \ {1}) = Subgroup.closure s
• Subgroup.closure_union_one 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.closure (s ∪ {1}) = Subgroup.closure s
• Subgroup.closure_le 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} : Subgroup.closure k ≤ K ↔ k ⊆ ↑K
• Subgroup.gi 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  (G : Type u_1) [Group G] : GaloisInsertion Subgroup.closure SetLike.coe
• Subgroup.closure_eq_bot_iff 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} : Subgroup.closure k = ⊥ ↔ k ⊆ {1}
• Subgroup.closure_union 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (s t : Set G) : Subgroup.closure (s ∪ t) = Subgroup.closure s ⊔ Subgroup.closure t
• Subgroup.iSup_eq_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {ι : Sort u_2} (p : ι → Subgroup G) : ⨆ i, p i = Subgroup.closure (⋃ i, ↑(p i))
• Subgroup.closure_eq_of_le 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (K : Subgroup G) {k : Set G} (h₁ : k ⊆ ↑K) (h₂ : K ≤ Subgroup.closure k) : Subgroup.closure k = K
• Subgroup.mem_closure_singleton 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {x y : G} : y ∈ Subgroup.closure {x} ↔ ∃ n, x ^ n = y
• Subgroup.mem_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} {x : G} : x ∈ Subgroup.closure k ↔ ∀ (K : Subgroup G), k ⊆ ↑K → x ∈ K
• Subgroup.closure_eq_top_of_mclosure_eq_top 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {S : Set G} (h : Submonoid.closure S = ⊤) : Subgroup.closure S = ⊤
• Subgroup.sup_eq_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (H H' : Subgroup G) : H ⊔ H' = Subgroup.closure (↑H ∪ ↑H')
• Subgroup.le_closure_toSubmonoid 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (S : Set G) : Submonoid.closure S ≤ (Subgroup.closure S).toSubmonoid
• Subgroup.mem_closure_pair 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {C : Type u_2} [CommGroup C] {x y z : C} : z ∈ Subgroup.closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z
• AddSubgroup.toSubgroup'_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (S : Set (Additive G)) : AddSubgroup.toSubgroup' (AddSubgroup.closure S) = Subgroup.closure (⇑Additive.ofMul ⁻¹' S)
• AddSubgroup.toSubgroup_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {A : Type u_2} [AddGroup A] (S : Set A) : AddSubgroup.toSubgroup (AddSubgroup.closure S) = Subgroup.closure (⇑Multiplicative.toAdd ⁻¹' S)
• Subgroup.toAddSubgroup'_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {A : Type u_2} [AddGroup A] (S : Set (Multiplicative A)) : Subgroup.toAddSubgroup' (Subgroup.closure S) = AddSubgroup.closure (⇑Multiplicative.ofAdd ⁻¹' S)
• Subgroup.toAddSubgroup_closure 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] (S : Set G) : Subgroup.toAddSubgroup (Subgroup.closure S) = AddSubgroup.closure (⇑Additive.toMul ⁻¹' S)
• Subgroup.closure_closure_coe_preimage 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} : Subgroup.closure (Subtype.val ⁻¹' k) = ⊤
• Subgroup.closure_induction 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} {p : (g : G) → g ∈ Subgroup.closure k → Prop} (mem : ∀ (x : G) (hx : x ∈ k), p x ⋯) (one : p 1 ⋯) (mul : ∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x hx → p y hy → p (x * y) ⋯) (inv : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p x hx → p x⁻¹ ⋯) {x : G} (hx : x ∈ Subgroup.closure k) : p x hx
• Subgroup.closure_induction₂ 📋 Mathlib.Algebra.Group.Subgroup.Lattice
  {G : Type u_1} [Group G] {k : Set G} {p : (x y : G) → x ∈ Subgroup.closure k → y ∈ Subgroup.closure k → Prop} (mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯) (one_left : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p 1 x ⋯ hx) (one_right : ∀ (x : G) (hx : x ∈ Subgroup.closure k), p x 1 hx ⋯) (mul_left : ∀ (x y z : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k) (hz : z ∈ Subgroup.closure k), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) (mul_right : ∀ (y z x : G) (hy : y ∈ Subgroup.closure k) (hz : z ∈ Subgroup.closure k) (hx : x ∈ Subgroup.closure k), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) (inv_left : ∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x y hx hy → p x⁻¹ y ⋯ hy) (inv_right : ∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x y hx hy → p x y⁻¹ hx ⋯) {x y : G} (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k) : p x y hx hy
• MonoidHom.map_closure 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_4} [Group N] (f : G →* N) (s : Set G) : Subgroup.map f (Subgroup.closure s) = Subgroup.closure (⇑f '' s)
• MonoidHom.closure_preimage_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_4} [Group N] (f : G →* N) (s : Set N) : Subgroup.closure (⇑f ⁻¹' s) ≤ Subgroup.comap f (Subgroup.closure s)
• MonoidHom.eq_of_eqOn_dense 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {M : Type u_6} [Monoid M] {s : Set G} (hs : Subgroup.closure s = ⊤) {f g : G →* M} (h : Set.EqOn (⇑f) (⇑g) s) : f = g
• MonoidHom.eqOn_closure 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [Group G] {M : Type u_6} [Monoid M] {f g : G →* M} {s : Set G} (h : Set.EqOn (⇑f) (⇑g) s) : Set.EqOn ⇑f ⇑g ↑(Subgroup.closure s)
• 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.closure_le_normalClosure 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {s : Set G} : Subgroup.closure s ≤ Subgroup.normalClosure s
• Subgroup.normalClosure_closure_eq_normalClosure 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {s : Set G} : Subgroup.normalClosure ↑(Subgroup.closure s) = Subgroup.normalClosure s
• Subgroup.normalizer_le_normalizer_closure 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.normalizer s ≤ Subgroup.normalizer ↑(Subgroup.closure s)
• Subgroup.normal_subgroupOf_closure_normalizer 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] (s : Set G) : ((Subgroup.closure s).subgroupOf (Subgroup.normalizer s)).Normal
• Subgroup.closure_prod 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {N : Type u_4} [Group N] {s : Set G} {t : Set N} (hs : 1 ∈ s) (ht : 1 ∈ t) : Subgroup.closure (s ×ˢ t) = (Subgroup.closure s).prod (Subgroup.closure t)
• Subgroup.le_normalizer_closure_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [Group G] {H : Subgroup G} {s : Set G} : H ≤ Subgroup.normalizer ↑(Subgroup.closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ Subgroup.closure s
• Subgroup.unop_closure 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [Group G] (s : Set Gᵐᵒᵖ) : (Subgroup.closure s).unop = Subgroup.closure (MulOpposite.op ⁻¹' s)
• Subgroup.op_closure 📋 Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
  {G : Type u_2} [Group G] (s : Set G) : (Subgroup.closure s).op = Subgroup.closure (MulOpposite.unop ⁻¹' s)
• Subgroup.zpowers_eq_closure 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
  {G : Type u_1} [Group G] (g : G) : Subgroup.zpowers g = Subgroup.closure {g}
• Subgroup.centralizer_closure 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.centralizer ↑(Subgroup.closure s) = Subgroup.centralizer s
• Subgroup.closure_le_centralizer_centralizer 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] (s : Set G) : Subgroup.closure s ≤ Subgroup.centralizer ↑(Subgroup.centralizer s)
• Subgroup.center_eq_infi' 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] {s : Set G} (hs : Subgroup.closure s = ⊤) : Subgroup.center G = ⨅ g, Subgroup.centralizer {↑g}
• Subgroup.center_eq_iInf 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] {s : Set G} (hs : Subgroup.closure s = ⊤) : Subgroup.center G = ⨅ g ∈ s, Subgroup.centralizer {g}
• Subgroup.closureCommGroupOfComm 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) : CommGroup ↥(Subgroup.closure k)
• Subgroup.isMulCommutative_closure 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] {k : Set G} (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) : IsMulCommutative ↥(Subgroup.closure k)
• Subgroup.instIsMulCommutative_closure 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} [Group G] {S : Type u_3} [SetLike S G] [MulMemClass S G] (s : S) [IsMulCommutative ↥s] : IsMulCommutative ↥(Subgroup.closure ↑s)
• Subgroup.closure_inv 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] (s : Set G) : Subgroup.closure s⁻¹ = Subgroup.closure s
• Subgroup.inv_subset_closure 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] (S : Set G) : S⁻¹ ⊆ ↑(Subgroup.closure S)
• Subgroup.closure_singleton_inv 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] (x : G) : Subgroup.closure {x⁻¹} = Subgroup.closure {x}
• Subgroup.closure_toSubmonoid 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] (S : Set G) : (Subgroup.closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)
• Set.mul_subgroupClosure 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) : s * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
• Set.subgroupClosure_mul 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) : ↑(Subgroup.closure s) * s = ↑(Subgroup.closure s)
• Subgroup.closure_pow_le 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} {n : ℕ} : Subgroup.closure (s ^ n) ≤ Subgroup.closure s
• Subgroup.closure_pow 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : Subgroup.closure (s ^ n) = Subgroup.closure s
• Subgroup.closure_mul_le 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] (S T : Set G) : Subgroup.closure (S * T) ≤ Subgroup.closure S ⊔ Subgroup.closure T
• Subgroup.sup_eq_closure_mul 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] (H K : Subgroup G) : H ⊔ K = Subgroup.closure (↑H * ↑K)
• Set.pow_mul_subgroupClosure 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) (n : ℕ) : s ^ n * ↑(Subgroup.closure s) = ↑(Subgroup.closure s)
• Set.subgroupClosure_mul_pow 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} (hs : s.Nonempty) (n : ℕ) : ↑(Subgroup.closure s) * s ^ n = ↑(Subgroup.closure s)
• Subgroup.smul_closure 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {α : Type u_1} {G : Type u_2} [Group G] [Monoid α] [MulDistribMulAction α G] (a : α) (s : Set G) : a • Subgroup.closure s = Subgroup.closure (a • s)
• Subgroup.closure_pow_anti 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} {m n : ℕ} (hmn : m ∣ n) : Subgroup.closure (s ^ n) ≤ Subgroup.closure (s ^ m)
• Subgroup.smul_mem_of_mem_closure_of_mem 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {X : Type u_5} [MulAction G X] {s : Set G} {t : Set X} (hs : ∀ g ∈ s, g⁻¹ ∈ s) (hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t) {g : G} (hg : g ∈ Subgroup.closure s) {x : X} (hx : x ∈ t) : g • x ∈ t
• Subgroup.closure_induction'' 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} {p : (g : G) → g ∈ Subgroup.closure s → Prop} (mem : ∀ (x : G) (hx : x ∈ s), p x ⋯) (inv_mem : ∀ (x : G) (hx : x ∈ s), p x⁻¹ ⋯) (one : p 1 ⋯) (mul : ∀ (x y : G) (hx : x ∈ Subgroup.closure s) (hy : y ∈ Subgroup.closure s), p x hx → p y hy → p (x * y) ⋯) {x : G} (h : x ∈ Subgroup.closure s) : p x h
• Subgroup.closure_induction_left 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} {p : (x : G) → x ∈ Subgroup.closure s → Prop} (one : p 1 ⋯) (mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x * y) ⋯) (inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ Subgroup.closure s), p y hy → p (x⁻¹ * y) ⋯) {x : G} (h : x ∈ Subgroup.closure s) : p x h
• Subgroup.closure_induction_right 📋 Mathlib.Algebra.Group.Subgroup.Pointwise
  {G : Type u_2} [Group G] {s : Set G} {p : (x : G) → x ∈ Subgroup.closure s → Prop} (one : p 1 ⋯) (mul_right : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯) (mul_inv_cancel : ∀ (x : G) (hx : x ∈ Subgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯) {x : G} (h : x ∈ Subgroup.closure s) : p x h
• FreeGroup.closure_range_of 📋 Mathlib.GroupTheory.FreeGroup.Basic
  (α : Type u_1) : Subgroup.closure (Set.range FreeGroup.of) = ⊤
• FreeGroup.range_map 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α : Type u} {β : Type v} {f : α → β} : (FreeGroup.map f).range = Subgroup.closure (FreeGroup.of '' Set.range f)
• FreeGroup.range_lift_eq_closure 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α : Type u} {β : Type v} [Group β] {f : α → β} : (FreeGroup.lift f).range = Subgroup.closure (Set.range f)
• FreeGroup.lift_surjective_iff_closure_range_eq_top 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {α : Type u} {β : Type v} [Group β] {f : α → β} : Function.Surjective ⇑(FreeGroup.lift f) ↔ Subgroup.closure (Set.range f) = ⊤
• FreeGroup.closure_eq_range 📋 Mathlib.GroupTheory.FreeGroup.Basic
  {β : Type v} [Group β] (s : Set β) : Subgroup.closure s = (FreeGroup.lift Subtype.val).range
• Subgroup.fg_iff 📋 Mathlib.GroupTheory.Finiteness
  {G : Type u_3} [Group G] (P : Subgroup G) : P.FG ↔ ∃ S, Subgroup.closure S = P ∧ S.Finite
• Group.fg_iff 📋 Mathlib.GroupTheory.Finiteness
  {G : Type u_3} [Group G] : Group.FG G ↔ ∃ S, Subgroup.closure S = ⊤ ∧ S.Finite
• Group.closure_finite_fg 📋 Mathlib.GroupTheory.Finiteness
  {G : Type u_3} [Group G] (s : Set G) [Finite ↑s] : Group.FG ↥(Subgroup.closure s)
• Group.fg_iff' 📋 Mathlib.GroupTheory.Finiteness
  {G : Type u_3} [Group G] : Group.FG G ↔ ∃ n S, S.card = n ∧ Subgroup.closure ↑S = ⊤
• Group.closure_finset_fg 📋 Mathlib.GroupTheory.Finiteness
  {G : Type u_3} [Group G] (s : Finset G) : Group.FG ↥(Subgroup.closure ↑s)
• commutator_eq_closure 📋 Mathlib.GroupTheory.Commutator.Basic
  (G : Type u_1) [Group G] : commutator G = Subgroup.closure (commutatorSet G)
• Subgroup.commutator_def 📋 Mathlib.GroupTheory.Commutator.Basic
  {G : Type u_1} [Group G] (H₁ H₂ : Subgroup G) : ⁅H₁, H₂⁆ = Subgroup.closure {g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g}
• Subgroup.closure_pi 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {η : Type u_2} {f : η → Type u_3} [(i : η) → Group (f i)] [Finite η] {s : (i : η) → Set (f i)} (hs : ∀ (i : η), 1 ∈ s i) : Subgroup.closure (Set.univ.pi fun i => s i) = Subgroup.pi Set.univ fun i => Subgroup.closure (s i)
• Subgroup.quotientCenterEmbedding 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ⊤) : G ⧸ Subgroup.center G ↪ ↑S → ↑(commutatorSet G)
• Subgroup.quotientCenterEmbedding_apply 📋 Mathlib.GroupTheory.GroupAction.Quotient
  {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ⊤) (g : G) (s : ↑S) : (Subgroup.quotientCenterEmbedding hS) (↑g) s = ⟨⁅g, ↑s⁆, ⋯⟩
• Subgroup.closure_toSubmonoid_of_finite 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Group G] [Finite G] {s : Set G} : (Subgroup.closure s).toSubmonoid = Submonoid.closure s
• Subgroup.closure_toSubmonoid_of_isOfFinOrder 📋 Mathlib.GroupTheory.OrderOfElement
  {G : Type u_1} [Group G] {s : Set G} (hs : ∀ x ∈ s, IsOfFinOrder x) : (Subgroup.closure s).toSubmonoid = Submonoid.closure s
• Subgroup.exists_of_mem_closure_range 📋 Mathlib.Algebra.Group.Subgroup.Finsupp
  {M : Type u_1} [CommGroup M] {ι : Type u_2} (f : ι → M) (x : M) [Fintype ι] (hx : x ∈ Subgroup.closure (Set.range f)) : ∃ a, x = ∏ i, f i ^ a i
• Subgroup.mem_closure_range_iff_of_fintype 📋 Mathlib.Algebra.Group.Subgroup.Finsupp
  {M : Type u_1} [CommGroup M] {ι : Type u_2} {f : ι → M} {x : M} [Fintype ι] : x ∈ Subgroup.closure (Set.range f) ↔ ∃ a, x = ∏ i, f i ^ a i
• Subgroup.exists_finsupp_of_mem_closure_range 📋 Mathlib.Algebra.Group.Subgroup.Finsupp
  {M : Type u_1} [CommGroup M] {ι : Type u_2} (f : ι → M) (x : M) (hx : x ∈ Subgroup.closure (Set.range f)) : ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2
• Subgroup.mem_closure_range_iff 📋 Mathlib.Algebra.Group.Subgroup.Finsupp
  {M : Type u_1} [CommGroup M] {ι : Type u_2} {f : ι → M} {x : M} : x ∈ Subgroup.closure (Set.range f) ↔ ∃ a, x = a.prod fun x1 x2 => f x1 ^ x2
• Subgroup.mem_closure_iff_of_fintype 📋 Mathlib.Algebra.Group.Subgroup.Finsupp
  {M : Type u_1} [CommGroup M] {x : M} {s : Set M} [Fintype ↑s] : x ∈ Subgroup.closure s ↔ ∃ a, x = ∏ i, ↑i ^ a i
• Subgroup.finsetSup_zpowers 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
  {G : Type u_1} [Group G] (s : Finset G) : s.sup Subgroup.zpowers = Subgroup.closure ↑s
• Equiv.Perm.support_closure_subset_union 📋 Mathlib.GroupTheory.Perm.Finite
  {α : Type u} [DecidableEq α] [Fintype α] (S : Set (Equiv.Perm α)) (a : Equiv.Perm α) : a ∈ Subgroup.closure S → ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
• Equiv.Perm.disjoint_closure_of_disjoint_support 📋 Mathlib.GroupTheory.Perm.Finite
  {α : Type u} [DecidableEq α] [Fintype α] {S T : Set (Equiv.Perm α)} (h : ∀ a ∈ S, ∀ b ∈ T, Disjoint a.support b.support) : Disjoint (Subgroup.closure S) (Subgroup.closure T)
• Equiv.Perm.disjoint_support_closure_of_disjoint_support 📋 Mathlib.GroupTheory.Perm.Finite
  {α : Type u} [DecidableEq α] [Fintype α] {S T : Set (Equiv.Perm α)} (h : ∀ a ∈ S, ∀ b ∈ T, Disjoint a.support b.support) (a : Equiv.Perm α) : a ∈ Subgroup.closure S → ∀ b ∈ Subgroup.closure T, Disjoint a.support b.support
• Equiv.Perm.closure_isSwap 📋 Mathlib.GroupTheory.Perm.Sign
  {α : Type u} [DecidableEq α] [Finite α] : Subgroup.closure {σ | σ.IsSwap} = ⊤
• Equiv.Perm.closure_isCycle 📋 Mathlib.GroupTheory.Perm.Closure
  {β : Type u_2} [Finite β] : Subgroup.closure {σ | σ.IsCycle} = ⊤
• Equiv.Perm.closure_prime_cycle_swap 📋 Mathlib.GroupTheory.Perm.Closure
  {α : Type u_1} [DecidableEq α] [Fintype α] {σ τ : Equiv.Perm α} (h0 : Nat.Prime (Fintype.card α)) (h1 : σ.IsCycle) (h2 : σ.support = Finset.univ) (h3 : τ.IsSwap) : Subgroup.closure {σ, τ} = ⊤
• Equiv.Perm.closure_cycle_adjacent_swap 📋 Mathlib.GroupTheory.Perm.Closure
  {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Equiv.Perm α} (h1 : σ.IsCycle) (h2 : σ.support = Finset.univ) (x : α) : Subgroup.closure {σ, Equiv.swap x (σ x)} = ⊤
• Equiv.Perm.closure_cycle_coprime_swap 📋 Mathlib.GroupTheory.Perm.Closure
  {α : Type u_1} [DecidableEq α] [Fintype α] {n : ℕ} {σ : Equiv.Perm α} (h0 : n.Coprime (Fintype.card α)) (h1 : σ.IsCycle) (h2 : σ.support = Finset.univ) (x : α) : Subgroup.closure {σ, Equiv.swap x ((σ ^ n) x)} = ⊤
• Equiv.Perm.IsSwap.mul_mem_closure_three_cycles 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {σ τ : Equiv.Perm α} (hσ : σ.IsSwap) (hτ : τ.IsSwap) : σ * τ ∈ Subgroup.closure {σ | σ.IsThreeCycle}
• Equiv.Perm.swap_mul_swap_same_mem_closure_three_cycles 📋 Mathlib.GroupTheory.Perm.Cycle.Type
  {α : Type u_1} [Fintype α] [DecidableEq α] {a b c : α} (ab : a ≠ b) (ac : a ≠ c) : Equiv.swap a b * Equiv.swap a c ∈ Subgroup.closure {σ | σ.IsThreeCycle}
• Group.rank_le 📋 Mathlib.GroupTheory.Rank
  {G : Type u_1} [Group G] [h : Group.FG G] {S : Finset G} (hS : Subgroup.closure ↑S = ⊤) : Group.rank G ≤ S.card
• Group.rank_spec 📋 Mathlib.GroupTheory.Rank
  (G : Type u_1) [Group G] [h : Group.FG G] : ∃ S, S.card = Group.rank G ∧ Subgroup.closure ↑S = ⊤
• Subgroup.rank_closure_finite_le_nat_card 📋 Mathlib.GroupTheory.Rank
  {G : Type u_1} [Group G] (s : Set G) [Finite ↑s] : Group.rank ↥(Subgroup.closure s) ≤ Nat.card ↑s
• Subgroup.rank_closure_finset_le_card 📋 Mathlib.GroupTheory.Rank
  {G : Type u_1} [Group G] (s : Finset G) : Group.rank ↥(Subgroup.closure ↑s) ≤ s.card
• Subgroup.closure_image_isMulIndecomposable_baseOf 📋 Mathlib.Algebra.Group.Irreducible.Indecomposable
  {ι : Type u_1} {G : Type u_3} {S : Type u_4} [CommGroup G] [LinearOrder S] [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S] (v : ι → G) (hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹) (f : G →* S) (hf : ∀ (i : ι), f (v i) ≠ 1) : Subgroup.closure (v '' IsMulIndecomposable.baseOf v f) = Subgroup.closure (Set.range v)
• MonoidWithZeroHom.valueGroup_def 📋 Mathlib.Algebra.GroupWithZero.Range
  {A : Type u_1} {B : Type u_2} [MonoidWithZero A] [MonoidWithZero B] (f : A →*₀ B) : f.valueGroup = Subgroup.closure ↑f.valueMonoid
• RootPairing.range_weylGroupToPerm 📋 Mathlib.LinearAlgebra.RootSystem.WeylGroup
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : P.weylGroupToPerm.range = Subgroup.closure (Set.range P.reflectionPerm)
• RootPairing.range_weylGroup_weightHom 📋 Mathlib.LinearAlgebra.RootSystem.WeylGroup
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : ((RootPairing.Equiv.weightHom P).domRestrict P.weylGroup).range = Subgroup.closure (Set.range P.reflection)
• RootPairing.range_weylGroup_coweightHom 📋 Mathlib.LinearAlgebra.RootSystem.WeylGroup
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) : ((RootPairing.Equiv.coweightHom P).domRestrict P.weylGroup).range = Subgroup.closure (Set.range (MulOpposite.op ∘ P.coreflection))
• Subgroup.cyclic_of_min 📋 Mathlib.GroupTheory.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (ha : IsLeast {g | g ∈ H ∧ 1 < g} a) : H = Subgroup.closure {a}
• Subgroup.cyclic_of_isolated_one 📋 Mathlib.GroupTheory.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {H : Subgroup G} {a : G} (h₀ : 1 < a) (hd : Disjoint (↑H) (Set.Ioo 1 a)) : ∃ b, H = Subgroup.closure {b}
• Subgroup.dense_or_cyclic 📋 Mathlib.Topology.Algebra.Order.Archimedean
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [TopologicalSpace G] [OrderTopology G] [MulArchimedean G] (S : Subgroup G) : Dense ↑S ∨ ∃ a, S = Subgroup.closure {a}
• LinearIsometryEquiv.reflections_generate 📋 Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
  {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] : Subgroup.closure (Set.range fun v => (ℝ ∙ v)ᗮ.reflection) = ⊤
• Subgroup.mem_closure_singleton_iff_existsUnique_zpow 📋 Mathlib.GroupTheory.ArchimedeanDensely
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] {a b : G} (ha : a ≠ 1) : b ∈ Subgroup.closure {a} ↔ ∃! k, a ^ k = b
• Subgroup.isLeast_of_closure_iff_eq_mabs 📋 Mathlib.GroupTheory.ArchimedeanDensely
  {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a b : G} : IsLeast {y | y ∈ Subgroup.closure {a} ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b
• LinearOrderedCommGroup.closure_equiv_closure 📋 Mathlib.GroupTheory.ArchimedeanDensely
  {G : Type u_1} {G' : Type u_2} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [CommGroup G'] [LinearOrder G'] [IsOrderedMonoid G'] (x : G) (y : G') (hxy : x = 1 ↔ y = 1) : ↥(Subgroup.closure {x}) ≃*o ↥(Subgroup.closure {y})
• Quiver.SchreierGraph.evalWord_mem_closure 📋 Mathlib.Combinatorics.Quiver.Schreier
  {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) (w : List (S × Bool)) : Quiver.SchreierGraph.evalWord ι w ∈ Subgroup.closure (Set.range ι)
• Quiver.SchreierGraph.exists_evalWord_of_mem_closure 📋 Mathlib.Combinatorics.Quiver.Schreier
  {M : Type u_1} [Group M] {S : Type u_2} (ι : S → M) {g : M} (hg : g ∈ Subgroup.closure (Set.range ι)) : ∃ w, Quiver.SchreierGraph.evalWord ι w = g
• Quiver.SchreierGraph.exists_mem_closure_of_path 📋 Mathlib.Combinatorics.Quiver.Schreier
  {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) {x : Quiver.SchreierGraph V ι} {y : Quiver.Symmetrify (Quiver.SchreierGraph V ι)} (p : Quiver.Path (Quiver.Symmetrify.of.obj x) y) : ∃ g ∈ Subgroup.closure (Set.range ι), g • x = y
• Quiver.SchreierGraph.reachable_of_mem_closure 📋 Mathlib.Combinatorics.Quiver.Schreier
  {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) {g : M} (hg : g ∈ Subgroup.closure (Set.range ι)) (y : Quiver.SchreierGraph V ι) : Quiver.Reachable (Quiver.Symmetrify.of.obj y) (Quiver.Symmetrify.of.obj (g • y))
• Quiver.SchreierGraph.reachable_iff 📋 Mathlib.Combinatorics.Quiver.Schreier
  {V : Type u_1} {M : Type u_2} [Group M] [MulAction M V] {S : Type u_3} (ι : S → M) (x y : Quiver.SchreierGraph V ι) : Quiver.Reachable (Quiver.Symmetrify.of.obj x) (Quiver.Symmetrify.of.obj y) ↔ ∃ g ∈ Subgroup.closure (Set.range ι), g • x = y
• Finset.pow_right_strictMono 📋 Mathlib.Geometry.Group.Growth.LinearLowerBound
  {G : Type u_1} [Group G] [DecidableEq G] {X : Finset G} (hX₁ : 1 ∈ X) (hXclosure : (↑(Subgroup.closure ↑X)).Infinite) : StrictMono fun n => X ^ n
• Finset.add_one_le_card_pow 📋 Mathlib.Geometry.Group.Growth.LinearLowerBound
  {G : Type u_1} [Group G] [DecidableEq G] {X : Finset G} (hX₁ : 1 ∈ X) (hXclosure : (↑(Subgroup.closure ↑X)).Infinite) (n : ℕ) : n + 1 ≤ (X ^ n).card
• Finset.pow_right_strictMonoOn 📋 Mathlib.Geometry.Group.Growth.LinearLowerBound
  {G : Type u_1} [Group G] [DecidableEq G] {X : Finset G} (hX₁ : 1 ∈ X) (hX : X.Nontrivial) : StrictMonoOn (fun n => X ^ n) {n | ↑X ^ (n - 1) ≠ ↑(Subgroup.closure ↑X)}
• Finset.pow_ssubset_pow_succ_of_pow_ne_closure 📋 Mathlib.Geometry.Group.Growth.LinearLowerBound
  {G : Type u_1} [Group G] [DecidableEq G] {X : Finset G} {n : ℕ} (hX₁ : 1 ∈ X) (hX : X.Nontrivial) (hXclosure : ↑X ^ n ≠ ↑(Subgroup.closure ↑X)) : X ^ n ⊂ X ^ (n + 1)
• Monoid.Coprod.closure_range_inl_union_inr 📋 Mathlib.GroupTheory.Coprod.Basic
  {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Subgroup.closure (Set.range ⇑Monoid.Coprod.inl ∪ Set.range ⇑Monoid.Coprod.inr) = ⊤
• PresentedGroup.closure_range_of 📋 Mathlib.GroupTheory.PresentedGroup
  {α : Type u_1} (rels : Set (FreeGroup α)) : Subgroup.closure (Set.range PresentedGroup.of) = ⊤
• CoxeterSystem.subgroup_closure_range_simple 📋 Mathlib.GroupTheory.Coxeter.Basic
  {B : Type u_1} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : Subgroup.closure (Set.range cs.simple) = ⊤
• Subgroup.closure_mul_image_eq 📋 Mathlib.GroupTheory.Schreier
  {G : Type u_1} [Group G] {H : Subgroup G} {R S : Set G} (hR : Subgroup.IsComplement (↑H) R) (hR1 : 1 ∈ R) (hS : Subgroup.closure S = ⊤) : Subgroup.closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S)) = H
• Subgroup.closure_mul_image_mul_eq_top 📋 Mathlib.GroupTheory.Schreier
  {G : Type u_1} [Group G] {H : Subgroup G} {R S : Set G} (hR : Subgroup.IsComplement (↑H) R) (hR1 : 1 ∈ R) (hS : Subgroup.closure S = ⊤) : ↑(Subgroup.closure ((fun g => g * (↑(hR.toRightFun g))⁻¹) '' (R * S))) * R = ⊤
• Subgroup.exists_finset_card_le_mul 📋 Mathlib.GroupTheory.Schreier
  {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] {S : Finset G} (hS : Subgroup.closure ↑S = ⊤) : ∃ T, T.card ≤ H.index * S.card ∧ Subgroup.closure ↑T = ⊤
• Subgroup.closure_mul_image_eq_top 📋 Mathlib.GroupTheory.Schreier
  {G : Type u_1} [Group G] {H : Subgroup G} {R S : Set G} (hR : Subgroup.IsComplement (↑H) R) (hR1 : 1 ∈ R) (hS : Subgroup.closure S = ⊤) : Subgroup.closure ((fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) '' (R * S)) = ⊤
• Subgroup.closure_mul_image_eq_top' 📋 Mathlib.GroupTheory.Schreier
  {G : Type u_1} [Group G] {H : Subgroup G} [DecidableEq G] {R S : Finset G} (hR : Subgroup.IsComplement ↑H ↑R) (hR1 : 1 ∈ R) (hS : Subgroup.closure ↑S = ⊤) : Subgroup.closure ↑(Finset.image (fun g => ⟨g * (↑(hR.toRightFun g))⁻¹, ⋯⟩) (R * S)) = ⊤
• Subgroup.focalSubgroup_def 📋 Mathlib.GroupTheory.Focal
  {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroup = Subgroup.closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
• Subgroup.focalSubgroupOf_eq_closure 📋 Mathlib.GroupTheory.Focal
  {G : Type u_1} [Group G] (H : Subgroup G) : H.focalSubgroupOf = Subgroup.closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}
• mem_lowerCentralSeries_succ_iff 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] (S : Subgroup G) (n : ℕ) (q : G) : q ∈ S.lowerCentralSeries (n + 1) ↔ q ∈ Subgroup.closure {x | ∃ p ∈ S.lowerCentralSeries n, ∃ q ∈ S, ⁅p, q⁆ = x}
• Subgroup.mem_lowerCentralSeries_succ_iff 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [Group G] (S : Subgroup G) (n : ℕ) (q : G) : q ∈ S.lowerCentralSeries (n + 1) ↔ q ∈ Subgroup.closure {x | ∃ p ∈ S.lowerCentralSeries n, ∃ q ∈ S, ⁅p, q⁆ = x}
• Group.Generators.ofSet 📋 Mathlib.GroupTheory.Generators
  {G : Type u_1} [Group G] {S : Set G} (h : Subgroup.closure S = ⊤) : Group.Generators G ↑S
• Group.Generators.mk 📋 Mathlib.GroupTheory.Generators
  {G : Type u_5} [Group G] {ι : Type u_6} (val : ι → G) (closure_eq_top : Subgroup.closure (Set.range val) = ⊤) : Group.Generators G ι
• Group.Generators.closure_eq_top 📋 Mathlib.GroupTheory.Generators
  {G : Type u_5} [Group G] {ι : Type u_6} (self : Group.Generators G ι) : Subgroup.closure (Set.range self.val) = ⊤
• Group.Generators.ofSet_val 📋 Mathlib.GroupTheory.Generators
  {G : Type u_1} [Group G] {S : Set G} (hS : Subgroup.closure S = ⊤) : (Group.Generators.ofSet hS).val = Subtype.val
• Equiv.Perm.closure_three_cycles_eq_alternating 📋 Mathlib.GroupTheory.SpecificGroups.Alternating
  {α : Type u_1} [Fintype α] [DecidableEq α] : Subgroup.closure {σ | σ.IsThreeCycle} = alternatingGroup α
• Equiv.Perm.closure_cycleType_eq_2_2_eq_alternatingGroup 📋 Mathlib.GroupTheory.SpecificGroups.Alternating
  {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Nat.card α) : Subgroup.closure {g | g.cycleType = {2, 2}} = alternatingGroup α
• Equiv.Perm.closure_cycleType_eq_two_two_eq_alternatingGroup 📋 Mathlib.GroupTheory.SpecificGroups.Alternating
  {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Nat.card α) : Subgroup.closure {g | g.cycleType = {2, 2}} = alternatingGroup α
• alternatingGroup.closure_isThreeCycles_eq_top 📋 Mathlib.GroupTheory.SpecificGroups.Alternating
  {α : Type u_1} [Fintype α] [DecidableEq α] : Subgroup.closure {g | (↑g).IsThreeCycle} = ⊤
• alternatingGroup.closure_cycleType_eq_two_two_eq_top 📋 Mathlib.GroupTheory.SpecificGroups.Alternating
  {α : Type u_1} [Fintype α] [DecidableEq α] (h5 : 5 ≤ Nat.card α) : Subgroup.closure {g | (↑g).cycleType = {2, 2}} = ⊤
• mem_closure_isSwap' 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {α : Type u_2} [DecidableEq α] {f : Equiv.Perm α} : f ∈ Subgroup.closure {σ | σ.IsSwap} ↔ (MulAction.fixedBy α f)ᶜ.Finite
• finite_compl_fixedBy_closure_iff 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {S : Set G} : (∀ g ∈ Subgroup.closure S, (MulAction.fixedBy α g)ᶜ.Finite) ↔ ∀ g ∈ S, (MulAction.fixedBy α g)ᶜ.Finite
• surjective_of_isSwap_of_isPretransitive 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Finite α] (S : Set G) (hS1 : ∀ σ ∈ S, ((MulAction.toPermHom G α) σ).IsSwap) (hS2 : Subgroup.closure S = ⊤) [h : MulAction.IsPretransitive G α] : Function.Surjective ⇑(MulAction.toPermHom G α)
• surjective_of_isSwap_of_isPretransitive' 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [DecidableEq α] [Finite α] (S : Set G) (hS1 : ∀ σ ∈ S, (MulAction.toPermHom G α) σ = 1 ∨ ((MulAction.toPermHom G α) σ).IsSwap) (hS2 : Subgroup.closure S = ⊤) [h : MulAction.IsPretransitive G α] : Function.Surjective ⇑(MulAction.toPermHom G α)
• exists_smul_notMem_of_subset_orbit_closure 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (S : Set G) (T : Set α) {a : α} (hS : ∀ g ∈ S, g⁻¹ ∈ S) (subset : T ⊆ MulAction.orbit (↥(Subgroup.closure S)) a) (notMem : a ∉ T) (nonempty : T.Nonempty) : ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T
• closure_of_isSwap_of_isPretransitive 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {α : Type u_2} [DecidableEq α] [Finite α] {S : Set (Equiv.Perm α)} (hS : ∀ σ ∈ S, σ.IsSwap) [MulAction.IsPretransitive (↥(Subgroup.closure S)) α] : Subgroup.closure S = ⊤
• swap_mem_closure_isSwap 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {α : Type u_2} [DecidableEq α] {S : Set (Equiv.Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {x y : α} : Equiv.swap x y ∈ Subgroup.closure S ↔ x ∈ MulAction.orbit (↥(Subgroup.closure S)) y
• mem_closure_isSwap 📋 Mathlib.GroupTheory.Perm.ClosureSwap
  {α : Type u_2} [DecidableEq α] {S : Set (Equiv.Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {f : Equiv.Perm α} : f ∈ Subgroup.closure S ↔ (MulAction.fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), f x ∈ MulAction.orbit (↥(Subgroup.closure S)) x
• SpecialLinearGroup.SL2Z_generators 📋 Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
  : Subgroup.closure {ModularGroup.S, ModularGroup.T} = ⊤
• NumberField.Units.closure_fundSystem_sup_torsion_eq_top 📋 Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
  (K : Type u_1) [Field K] [NumberField K] : Subgroup.closure (Set.range (NumberField.Units.fundSystem K)) ⊔ NumberField.Units.torsion K = ⊤
• SlashInvariantForm.slash_action_generators 📋 Mathlib.NumberTheory.ModularForms.Identities
  {f : UpperHalfPlane → ℂ} {Γ : Subgroup (GL (Fin 2) ℝ)} {s : Set (GL (Fin 2) ℝ)} (hΓ : Γ = Subgroup.closure s) {k : ℤ} : (∀ γ ∈ Γ, SlashAction.map k γ f = f) ↔ ∀ γ ∈ s, SlashAction.map k γ f = f
• NumberField.Units.isMaxRank_iff_closure_finiteIndex 📋 Mathlib.NumberTheory.NumberField.Units.Regulator
  {K : Type u_1} [Field K] [NumberField K] {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} : NumberField.Units.IsMaxRank u ↔ (Subgroup.closure (Set.range u)).FiniteIndex
• NumberField.Units.regOfFamily_div_regulator 📋 Mathlib.NumberTheory.NumberField.Units.Regulator
  {K : Type u_1} [Field K] [NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) : NumberField.Units.regOfFamily u / NumberField.Units.regulator K = ↑(Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K).index
• NumberField.Units.regOfFamily_div_regOfFamily 📋 Mathlib.NumberTheory.NumberField.Units.Regulator
  {K : Type u_1} [Field K] [NumberField K] {u v : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hv : NumberField.Units.IsMaxRank v) (h : Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K ≤ Subgroup.closure (Set.range v) ⊔ NumberField.Units.torsion K) : NumberField.Units.regOfFamily u / NumberField.Units.regOfFamily v = ↑((Subgroup.closure (Set.range u) ⊔ NumberField.Units.torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ NumberField.Units.torsion K))
• NumberField.Units.span_basisOfIsMaxRank 📋 Mathlib.NumberTheory.NumberField.Units.Regulator
  {K : Type u_1} [Field K] [NumberField K] {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ} (hu : NumberField.Units.IsMaxRank u) : (Submodule.span ℤ (Set.range ⇑(NumberField.Units.basisOfIsMaxRank hu))).toAddSubgroup = AddSubgroup.map (NumberField.Units.logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))
• NumberField.IsCMField.closure_realFundSystem_sup_torsion 📋 Mathlib.NumberTheory.NumberField.CMField
  (K : Type u_1) [Field K] [CharZero K] [NumberField.IsCMField K] [NumberField K] : Subgroup.closure (Set.range (NumberField.IsCMField.realFundSystem K)) ⊔ NumberField.Units.torsion K = NumberField.IsCMField.realUnits K ⊔ NumberField.Units.torsion K
• dense_submonoidClosure_iff_subgroupClosure 📋 Mathlib.Topology.Algebra.Group.SubmonoidClosure
  {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {s : Set G} : Dense ↑(Submonoid.closure s) ↔ Dense ↑(Subgroup.closure s)
• closure_submonoidClosure_eq_closure_subgroupClosure 📋 Mathlib.Topology.Algebra.Group.SubmonoidClosure
  {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (s : Set G) : closure ↑(Submonoid.closure s) = closure ↑(Subgroup.closure s)
• topologicalClosure_subgroupClosure_toSubmonoid 📋 Mathlib.Topology.Algebra.Group.SubmonoidClosure
  {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (s : Set G) : (Subgroup.closure s).topologicalClosure = (Submonoid.closure s).topologicalClosure

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 ce5dd8c