Loogle!

Result

Found 132 declarations mentioning AddSubgroup.map.

• AddSubgroup.map_id 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) : AddSubgroup.map (AddMonoidHom.id G) K = K
• AddSubgroup.map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup N
• AddSubgroup.map_bot 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.map f ⊥ = ⊥
• AddSubgroup.addSubgroupOf_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) : AddSubgroup.map K.subtype (H.addSubgroupOf K) = H ⊓ K
• AddSubgroup.le_comap_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : H ≤ AddSubgroup.comap f (AddSubgroup.map f H)
• AddSubgroup.map_comap_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) ≤ H
• AddSubgroup.gc_map_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)
• AddSubgroup.map_addSubgroupOf_eq_of_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) : AddSubgroup.map K.subtype (H.addSubgroupOf K) = H
• AddSubgroup.map_iSup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} (f : G →+ N) (s : ι → AddSubgroup G) : AddSubgroup.map f (iSup s) = ⨆ i, AddSubgroup.map f (s i)
• AddSubgroup.map_zero_eq_bot 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] : AddSubgroup.map 0 K = ⊥
• AddSubgroup.map_isAddCommutative 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [IsAddCommutative ↥H] : IsAddCommutative ↥(AddSubgroup.map f H)
• AddSubgroup.map_isCommutative 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') [IsAddCommutative ↥H] : IsAddCommutative ↥(AddSubgroup.map f H)
• AddMonoidHom.map_closure 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (s : Set G) : AddSubgroup.map f (AddSubgroup.closure s) = AddSubgroup.closure (⇑f '' s)
• AddSubgroup.map_inf_le 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) : AddSubgroup.map f (H ⊓ K) ≤ AddSubgroup.map f H ⊓ AddSubgroup.map f K
• AddSubgroup.map_top_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (h : Function.Surjective ⇑f) : AddSubgroup.map f ⊤ = ⊤
• AddSubgroup.map_mono 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K K' : AddSubgroup G} : K ≤ K' → AddSubgroup.map f K ≤ AddSubgroup.map f K'
• AddSubgroup.map_le_iff_le_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {H : AddSubgroup N} : AddSubgroup.map f K ≤ H ↔ K ≤ AddSubgroup.comap f H
• AddSubgroup.map_sup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) : AddSubgroup.map f (H ⊔ K) = AddSubgroup.map f H ⊔ AddSubgroup.map f K
• AddSubgroup.coe_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) : ↑(AddSubgroup.map f K) = ⇑f '' ↑K
• AddSubgroup.map_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {P : Type u_6} [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.map g (AddSubgroup.map f K) = AddSubgroup.map (g.comp f) K
• AddSubgroup.mem_map_of_mem 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {K : AddSubgroup G} {x : G} (hx : x ∈ K) : f x ∈ AddSubgroup.map f K
• AddSubgroup.comap_equiv_eq_map_symm' 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : N ≃+ G) (K : AddSubgroup G) : AddSubgroup.comap f.toAddMonoidHom K = AddSubgroup.map f.symm.toAddMonoidHom K
• AddSubgroup.map_equiv_eq_comap_symm' 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G ≃+ N) (K : AddSubgroup G) : AddSubgroup.map f.toAddMonoidHom K = AddSubgroup.comap f.symm.toAddMonoidHom K
• AddSubgroup.map_iInf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {ι : Sort u_7} [Nonempty ι] (f : G →+ N) (hf : Function.Injective ⇑f) (s : ι → AddSubgroup G) : AddSubgroup.map f (iInf s) = ⨅ i, AddSubgroup.map f (s i)
• AddSubgroup.map_inf 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
• AddSubgroup.map_inf_eq 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H K : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : AddSubgroup.map f (H ⊓ K) = AddSubgroup.map f H ⊓ AddSubgroup.map f K
• AddSubgroup.mem_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {K : AddSubgroup G} {y : N} : y ∈ AddSubgroup.map f K ↔ ∃ x ∈ K, f x = y
• AddSubgroup.map_toAddSubmonoid 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (K : AddSubgroup G) : (AddSubgroup.map f K).toAddSubmonoid = AddSubmonoid.map f K.toAddSubmonoid
• AddSubgroup.apply_coe_mem_map 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (K : AddSubgroup G) (x : ↥K) : f ↑x ∈ AddSubgroup.map f K
• AddSubgroup.equivMapOfInjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : ↥H ≃+ ↥(AddSubgroup.map f H)
• AddSubgroup.map.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.map f H = { carrier := ⇑f '' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
• AddSubgroup.mem_map_iff_mem 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {K : AddSubgroup G} {x : G} : f x ∈ AddSubgroup.map f K ↔ x ∈ K
• AddSubgroup.mem_map_equiv 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G ≃+ N} {K : AddSubgroup G} {x : N} : x ∈ AddSubgroup.map f.toAddMonoidHom K ↔ f.symm x ∈ K
• AddEquiv.coe_mapAddSubgroup 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {H : Type u_5} [AddGroup H] (e : G ≃+ H) : ⇑e.mapAddSubgroup = AddSubgroup.map e.toAddMonoidHom
• AddMonoidHom.addSubgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : ↥H →+ ↥(AddSubgroup.map f H)
• AddSubgroup.map_eq_comap_of_inverse 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {g : N →+ G} (hl : Function.LeftInverse ⇑g ⇑f) (hr : Function.RightInverse ⇑g ⇑f) (H : AddSubgroup G) : AddSubgroup.map f H = AddSubgroup.comap g H
• AddMonoidHom.addSubgroupMap.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : f.addSubgroupMap H = f.addSubmonoidMap H.toAddSubmonoid
• AddSubgroup.equivMapOfInjective.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) : H.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_add' := ⋯ }
• AddEquiv.mapAddSubgroup_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {H : Type u_6} [AddGroup H] (f : G ≃+ H) (H✝ : AddSubgroup G) : f.mapAddSubgroup H✝ = AddSubgroup.map (↑f) H✝
• AddEquiv.mapAddSubgroup_symm_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {H : Type u_6} [AddGroup H] (f : G ≃+ H) (H✝ : AddSubgroup H) : (RelIso.symm f.mapAddSubgroup) H✝ = AddSubgroup.map (↑f.symm) H✝
• AddEquiv.mapAddSubgroup.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {H : Type u_6} [AddGroup H] (f : G ≃+ H) : f.mapAddSubgroup = { toFun := AddSubgroup.map ↑f, invFun := AddSubgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
• AddSubgroup.comap_equiv_eq_map_symm 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : N ≃+ G) (K : AddSubgroup G) : AddSubgroup.comap (↑f) K = AddSubgroup.map (↑f.symm) K
• AddSubgroup.map_equiv_eq_comap_symm 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G ≃+ N) (K : AddSubgroup G) : AddSubgroup.map (↑f) K = AddSubgroup.comap (↑f.symm) K
• AddSubgroup.map_symm_eq_iff_map_eq 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) {N : Type u_5} [AddGroup N] {H : AddSubgroup N} {e : G ≃+ N} : AddSubgroup.map (↑e.symm) H = K ↔ AddSubgroup.map (↑e) K = H
• AddEquiv.addSubgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) : ↥H ≃+ ↥(AddSubgroup.map (↑e) H)
• AddEquiv.addSubgroupMap.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) : e.addSubgroupMap H = e.addSubmonoidMap H.toAddSubmonoid
• AddSubgroup.coe_equivMapOfInjective_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) (hf : Function.Injective ⇑f) (h : ↥H) : ↑((H.equivMapOfInjective f hf) h) = f ↑h
• AddMonoidHom.addSubgroupMap_surjective 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) : Function.Surjective ⇑(f.addSubgroupMap H)
• AddSubgroup.equivMapOfInjective_coe_addEquiv 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G') : H.equivMapOfInjective ↑e ⋯ = e.addSubgroupMap H
• AddMonoidHom.addSubgroupMap_apply_coe 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (H : AddSubgroup G) (x : ↥H.toAddSubmonoid) : ↑((f.addSubgroupMap H) x) = f ↑x
• AddEquiv.coe_addSubgroupMap_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : ↥H) : ↑((e.addSubgroupMap H) g) = e ↑g
• AddEquiv.addSubgroupMap_symm_apply 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (e : G ≃+ G') (H : AddSubgroup G) (g : ↥(AddSubgroup.map (↑e) H)) : (e.addSubgroupMap H).symm g = ⟨e.symm ↑g, ⋯⟩
• AddMonoidHom.range_eq_map 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range = AddSubgroup.map f ⊤
• AddSubgroup.map_comap_eq 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) = f.range ⊓ H
• AddSubgroup.map_le_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.map f H ≤ f.range
• AddSubgroup.map_comap_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup N} (h : H ≤ f.range) : AddSubgroup.map f (AddSubgroup.comap f H) = H
• AddSubgroup.comap_map_eq 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) (H : AddSubgroup G) : AddSubgroup.comap f (AddSubgroup.map f H) = H ⊔ f.ker
• AddSubgroup.map_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) : Function.Injective (AddSubgroup.map f)
• AddSubgroup.comap_map_eq_self 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} (h : f.ker ≤ H) : AddSubgroup.comap f (AddSubgroup.map f H) = H
• AddSubgroup.map_eq_bot_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} : AddSubgroup.map f H = ⊥ ↔ H ≤ f.ker
• AddSubgroup.map_subtype_le 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) : AddSubgroup.map H.subtype K ≤ H
• AddSubgroup.comap_map_eq_self_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Injective ⇑f) (H : AddSubgroup G) : AddSubgroup.comap f (AddSubgroup.map f H) = H
• AddSubgroup.map_comap_eq_self_of_surjective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (h : Function.Surjective ⇑f) (H : AddSubgroup N) : AddSubgroup.map f (AddSubgroup.comap f H) = H
• AddMonoidHom.map_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : AddSubgroup.map g f.range = (g.comp f).range
• AddMonoidHom.range_comp 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} {P : Type u_6} [AddGroup N] [AddGroup P] (g : N →+ P) (f : G →+ N) : (g.comp f).range = AddSubgroup.map g f.range
• AddMonoidHom.range.eq_1 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) : f.range = (AddSubgroup.map f ⊤).copy (Set.range ⇑f) ⋯
• AddSubgroup.map_eq_bot_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Injective ⇑f) : AddSubgroup.map f H = ⊥ ↔ H = ⊥
• AddMonoidHom.restrict_range 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (K : AddSubgroup G) (f : G →+ N) : (f.restrict K).range = AddSubgroup.map f K
• AddSubgroup.map_eq_range_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H : AddSubgroup G} : AddSubgroup.map f H = f.range ↔ Codisjoint H f.ker
• AddSubgroup.map_eq_map_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : AddSubgroup.map f H = AddSubgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
• AddSubgroup.map_le_map_iff 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K ⊔ f.ker
• AddSubgroup.map_injective_of_ker_le 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (f : G →+ N) {H K : AddSubgroup G} (hH : f.ker ≤ H) (hK : f.ker ≤ K) (hf : AddSubgroup.map f H = AddSubgroup.map f K) : H = K
• AddSubgroup.map_le_map_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ≤ K
• AddSubgroup.map_lt_map_iff_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} (hf : Function.Injective ⇑f) {H K : AddSubgroup G} : AddSubgroup.map f H < AddSubgroup.map f K ↔ H < K
• AddSubgroup.map_le_map_iff' 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {f : G →+ N} {H K : AddSubgroup G} : AddSubgroup.map f H ≤ AddSubgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
• AddSubgroup.ker_addSubgroupMap 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G →+ N) : (f.addSubgroupMap H).ker = f.ker.addSubgroupOf H
• AddSubgroup.map_subtype_le_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {G' : AddSubgroup G} {H K : AddSubgroup ↥G'} : AddSubgroup.map G'.subtype H ≤ AddSubgroup.map G'.subtype K ↔ H ≤ K
• AddSubgroup.map_subtype_lt_map_subtype 📋 Mathlib.Algebra.Group.Subgroup.Ker
  {G : Type u_1} [AddGroup G] {G' : AddSubgroup G} {H K : AddSubgroup ↥G'} : AddSubgroup.map G'.subtype H < AddSubgroup.map G'.subtype K ↔ H < K
• Submodule.map_toAddSubgroup 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] (f : M →ₗ[R] M₂) (p : Submodule R M) : (Submodule.map f p).toAddSubgroup = AddSubgroup.map (↑f) p.toAddSubgroup
• AddMonoidHom.coe_toMultiplicative_map 📋 Mathlib.Algebra.Module.Submodule.Map
  {G : Type u_10} {G₂ : Type u_11} [AddGroup G] [AddGroup G₂] (f : G →+ G₂) (s : AddSubgroup G) : Subgroup.map (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.map f s)
• MonoidHom.coe_toAdditive_map 📋 Mathlib.Algebra.Module.Submodule.Map
  {G : Type u_10} {G₂ : Type u_11} [Group G] [Group G₂] (f : G →* G₂) (s : Subgroup G) : AddSubgroup.map (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.map f s)
• AddMonoidHom.coe_toIntLinearMap_map 📋 Mathlib.Algebra.Module.Submodule.Map
  {A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A) : Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
• AddSubgroup.characteristic_iff_map_eq 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H = H
• AddSubgroup.le_normalizer_map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} {N : Type u_5} [AddGroup N] (f : G →+ N) : AddSubgroup.map f H.normalizer ≤ (AddSubgroup.map f H).normalizer
• AddSubgroup.characteristic_iff_le_map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), H ≤ AddSubgroup.map ϕ.toAddMonoidHom H
• AddSubgroup.characteristic_iff_map_le 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} : H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.map ϕ.toAddMonoidHom H ≤ H
• AddSubgroup.Normal.map 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} (h : H.Normal) (f : G →+ N) (hf : Function.Surjective ⇑f) : (AddSubgroup.map f H).Normal
• AddSubgroup.map_equiv_normalizer_eq 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) (f : G ≃+ N) : AddSubgroup.map f.toAddMonoidHom H.normalizer = (AddSubgroup.map f.toAddMonoidHom H).normalizer
• AddSubgroup.map_normalizer_eq_of_bijective 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] (H : AddSubgroup G) {f : G →+ N} (hf : Function.Bijective ⇑f) : AddSubgroup.map f H.normalizer = (AddSubgroup.map f H).normalizer
• AddSubgroup.le_pi_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {η : Type u_7} {f : η → Type u_8} [(i : η) → AddGroup (f i)] {I : Set η} {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} : J ≤ AddSubgroup.pi I H ↔ ∀ i ∈ I, AddSubgroup.map (Pi.evalAddMonoidHom f i) J ≤ H i
• AddSubgroup.le_prod_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} : J ≤ H.prod K ↔ AddSubgroup.map (AddMonoidHom.fst G N) J ≤ H ∧ AddSubgroup.map (AddMonoidHom.snd G N) J ≤ K
• AddSubgroup.prod_le_iff 📋 Mathlib.Algebra.Group.Subgroup.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_5} [AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N} {J : AddSubgroup (G × N)} : H.prod K ≤ J ↔ AddSubgroup.map (AddMonoidHom.inl G N) H ≤ J ∧ AddSubgroup.map (AddMonoidHom.inr G N) K ≤ J
• AddMonoidHom.map_zmultiples 📋 Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
  {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] (f : G →+ N) (x : G) : AddSubgroup.map f (AddSubgroup.zmultiples x) = AddSubgroup.zmultiples (f x)
• AddSubgroup.map_centralizer_le_centralizer_image 📋 Mathlib.GroupTheory.Subgroup.Centralizer
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (s : Set G) (f : G →+ G') : AddSubgroup.map f (AddSubgroup.centralizer s) ≤ AddSubgroup.centralizer (⇑f '' s)
• AddSubgroup.pointwise_smul_def 📋 Mathlib.Algebra.GroupWithZero.Subgroup
  {M : Type u_3} {A : Type u_4} [Monoid M] [AddGroup A] [DistribMulAction M A] {a : M} (S : AddSubgroup A) : a • S = AddSubgroup.map ((DistribMulAction.toAddMonoidEnd M A) a) S
• AddSubgroup.card_map_of_injective 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {G : Type u_1} [AddGroup G] {H : Type u_3} [AddGroup H] {K : AddSubgroup G} {f : G →+ H} (hf : Function.Injective ⇑f) : Nat.card ↥(AddSubgroup.map f K) = Nat.card ↥K
• AddSubgroup.pi_le_iff 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {η : Type u_3} {f : η → Type u_4} [(i : η) → AddGroup (f i)] [DecidableEq η] [Finite η] {H : (i : η) → AddSubgroup (f i)} {J : AddSubgroup ((i : η) → f i)} : AddSubgroup.pi Set.univ H ≤ J ↔ ∀ (i : η), AddSubgroup.map (AddMonoidHom.single f i) (H i) ≤ J
• AddSubgroup.card_subtype 📋 Mathlib.Algebra.Group.Subgroup.Finite
  {G : Type u_1} [AddGroup G] (K : AddSubgroup G) (L : AddSubgroup ↥K) : Nat.card ↥(AddSubgroup.map K.subtype L) = Nat.card ↥L
• QuotientAddGroup.map_mk'_self 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : AddSubgroup.map (QuotientAddGroup.mk' N) N = ⊥
• QuotientAddGroup.ker_lift 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {M : Type x} [AddMonoid M] (φ : G →+ M) (HN : N ≤ φ.ker) : (QuotientAddGroup.lift N φ HN).ker = AddSubgroup.map (QuotientAddGroup.mk' N) φ.ker
• QuotientAddGroup.ker_map 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] (M : AddSubgroup H) [M.Normal] (f : G →+ H) (h : N ≤ AddSubgroup.comap f M) : (QuotientAddGroup.map N M f h).ker = AddSubgroup.map (QuotientAddGroup.mk' N) (AddSubgroup.comap f M)
• QuotientAddGroup.congr 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : G ⧸ G' ≃+ H ⧸ H'
• QuotientAddGroup.congr.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Defs
  {G : Type u} [AddGroup G] {H : Type v} [AddGroup H] (G' : AddSubgroup G) (H' : AddSubgroup H) [G'.Normal] [H'.Normal] (e : G ≃+ H) (he : AddSubgroup.map (↑e) G' = H') : QuotientAddGroup.congr G' H' e he = { toFun := ⇑(QuotientAddGroup.map G' H' ↑e ⋯), invFun := ⇑(QuotientAddGroup.map H' G' ↑e.symm ⋯), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
• QuotientAddGroup.map_normal 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] : (AddSubgroup.map (QuotientAddGroup.mk' N) M).Normal
• QuotientAddGroup.comap_map_mk' 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N H : AddSubgroup G) [N.Normal] : AddSubgroup.comap (QuotientAddGroup.mk' N) (AddSubgroup.map (QuotientAddGroup.mk' N) H) = N ⊔ H
• QuotientAddGroup.strictMono_comap_prod_map 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] : StrictMono fun H => (AddSubgroup.comap N.subtype H, AddSubgroup.map (QuotientAddGroup.mk' N) H)
• QuotientAddGroup.quotientQuotientEquivQuotientAux 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M →+ G ⧸ M
• QuotientAddGroup.quotientQuotientEquivQuotient 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : (G ⧸ N) ⧸ AddSubgroup.map (QuotientAddGroup.mk' N) M ≃+ G ⧸ M
• QuotientAddGroup.quotientQuotientEquivQuotientAux.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : QuotientAddGroup.quotientQuotientEquivQuotientAux N M h = QuotientAddGroup.lift (AddSubgroup.map (QuotientAddGroup.mk' N) M) (QuotientAddGroup.map N M (AddMonoidHom.id G) h) ⋯
• QuotientAddGroup.comapMk'OrderIso.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [hn : N.Normal] : QuotientAddGroup.comapMk'OrderIso N = { toFun := fun H' => ⟨AddSubgroup.comap (QuotientAddGroup.mk' N) H', ⋯⟩, invFun := fun H => AddSubgroup.map (QuotientAddGroup.mk' N) ↑H, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
• QuotientAddGroup.quotientQuotientEquivQuotient.eq_1 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) : QuotientAddGroup.quotientQuotientEquivQuotient N M h = (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h).toAddEquiv (QuotientAddGroup.map M (AddSubgroup.map (QuotientAddGroup.mk' N) M) (QuotientAddGroup.mk' N) ⋯) ⋯ ⋯
• QuotientAddGroup.quotientQuotientEquivQuotientAux_mk_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G) : (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑↑x = ↑x
• QuotientAddGroup.quotientQuotientEquivQuotientAux_mk 📋 Mathlib.GroupTheory.QuotientGroup.Basic
  {G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (M : AddSubgroup G) [nM : M.Normal] (h : N ≤ M) (x : G ⧸ N) : (QuotientAddGroup.quotientQuotientEquivQuotientAux N M h) ↑x = (QuotientAddGroup.map N M (AddMonoidHom.id G) h) x
• AddAction.stabilizer_vadd_eq_stabilizer_map_conj 📋 Mathlib.GroupTheory.GroupAction.Basic
  {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (g : G) (a : α) : AddAction.stabilizer G (g +ᵥ a) = AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) (AddAction.stabilizer G a)
• AddAction.stabilizerEquivStabilizerOfOrbitRel.eq_1 📋 Mathlib.GroupTheory.GroupAction.Basic
  {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {a b : α} (h : (AddAction.orbitRel G α) a b) : AddAction.stabilizerEquivStabilizerOfOrbitRel h = (AddEquiv.addSubgroupCongr ⋯).trans (AddEquiv.addSubgroupMap (AddAut.conj (Classical.choose h)) (AddAction.stabilizer G b)).symm
• AddSubgroup.relindex_comap 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G' →+ G) (K : AddSubgroup G') : (AddSubgroup.comap f H).relindex K = H.relindex (AddSubgroup.map f K)
• AddSubgroup.relindex_ker 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (K : AddSubgroup G) (f : G →+ G') : f.ker.relindex K = Nat.card ↥(AddSubgroup.map f K)
• AddSubgroup.card_map_dvd 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') : Nat.card ↥(AddSubgroup.map f H) ∣ Nat.card ↥H
• AddSubgroup.dvd_index_map 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf : f.ker ≤ H) : H.index ∣ (AddSubgroup.map f H).index
• AddSubgroup.index_map_of_bijective 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {f : G →+ G'} (hf : Function.Bijective ⇑f) (H : AddSubgroup G) : (AddSubgroup.map f H).index = H.index
• AddSubgroup.index_map_dvd 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf : Function.Surjective ⇑f) : (AddSubgroup.map f H).index ∣ H.index
• AddSubgroup.index_map 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) (f : G →+ G') : (AddSubgroup.map f H).index = (H ⊔ f.ker).index * f.range.index
• AddSubgroup.index_map_subtype 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (K : AddSubgroup ↥H) : (AddSubgroup.map H.subtype K).index = K.index * H.index
• AddSubgroup.index_map_of_injective 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf : Function.Injective ⇑f) : (AddSubgroup.map f H).index = H.index * f.range.index
• AddSubgroup.index_map_eq 📋 Mathlib.GroupTheory.Index
  {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (H : AddSubgroup G) {f : G →+ G'} (hf1 : Function.Surjective ⇑f) (hf2 : f.ker ≤ H) : (AddSubgroup.map f H).index = H.index
• DenseRange.topologicalClosure_map_addSubgroup 📋 Mathlib.Topology.Algebra.Group.Basic
  {G : Type w} {H : Type x} [TopologicalSpace G] [AddGroup G] [IsTopologicalAddGroup G] [AddGroup H] [TopologicalSpace H] [IsTopologicalAddGroup H] {f : G →+ H} (hf : Continuous ⇑f) (hf' : DenseRange ⇑f) {s : AddSubgroup G} (hs : s.topologicalClosure = ⊤) : (AddSubgroup.map f s).topologicalClosure = ⊤
• NormedAddGroupHom.comp_range 📋 Mathlib.Analysis.Normed.Group.Hom
  {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [SeminormedAddCommGroup V₁] [SeminormedAddCommGroup V₂] [SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂) (g : NormedAddGroupHom V₂ V₃) : (g.comp f).range = AddSubgroup.map g.toAddMonoidHom f.range
• AddAction.map_stabilizer_le 📋 Mathlib.Algebra.Pointwise.Stabilizer
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (f : G →+ H) (s : Set G) : AddSubgroup.map f (AddAction.stabilizer G s) ≤ AddAction.stabilizer H (⇑f '' s)
• AddSubgroup.goursatFst.eq_1 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (I : AddSubgroup (G × H)) : I.goursatFst = AddSubgroup.map ((AddMonoidHom.fst G H).comp I.subtype) ((AddMonoidHom.snd G H).comp I.subtype).ker
• AddSubgroup.goursatSnd.eq_1 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] (I : AddSubgroup (G × H)) : I.goursatSnd = AddSubgroup.map ((AddMonoidHom.snd G H).comp I.subtype) ((AddMonoidHom.fst G H).comp I.subtype).ker
• AddSubgroup.goursat 📋 Mathlib.GroupTheory.Goursat
  {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] {I : AddSubgroup (G × H)} : ∃ G' H' M N, ∃ (x : M.Normal) (x_1 : N.Normal), ∃ e, I = AddSubgroup.map (G'.subtype.prodMap H'.subtype) (AddSubgroup.comap ((QuotientAddGroup.mk' M).prodMap (QuotientAddGroup.mk' N)) e.toAddMonoidHom.graph)
• AddAction.IsBlock.of_addSubgroup_of_conjugate 📋 Mathlib.GroupTheory.GroupAction.Blocks
  {G : Type u_3} [AddGroup G] {X : Type u_4} [AddAction G X] {B : Set X} {H : AddSubgroup G} (hB : AddAction.IsBlock (↥H) B) (g : G) : AddAction.IsBlock (↥(AddSubgroup.map (AddEquiv.toAddMonoidHom (Additive.toMul (AddAut.conj g))) H)) (g +ᵥ B)

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:

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.

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