Loogle!
Result
Found 16 declarations mentioning QuotientAddGroup.map.
- QuotientAddGroup.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) : G ⧸ N â+ H ⧸ M - 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.map_id đ Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : N ⤠AddSubgroup.comap (AddMonoidHom.id G) N := âŻ) : QuotientAddGroup.map N N (AddMonoidHom.id G) h = AddMonoidHom.id (G ⧸ N) - QuotientAddGroup.map.eq_1 đ 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 = QuotientAddGroup.lift N ((QuotientAddGroup.mk' M).comp f) ⯠- QuotientAddGroup.map.congr_simp đ 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 fâ : G â+ H) (e_f : f = fâ) (h : N ⤠AddSubgroup.comap f M) : QuotientAddGroup.map N M f h = QuotientAddGroup.map N M fâ ⯠- QuotientAddGroup.map_id_apply đ Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] (h : N ⤠AddSubgroup.comap (AddMonoidHom.id G) N := âŻ) (x : G ⧸ N) : (QuotientAddGroup.map N N (AddMonoidHom.id G) h) x = x - QuotientAddGroup.map_mk đ 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) (x : G) : (QuotientAddGroup.map N M f h) âx = â(f x) - QuotientAddGroup.map_surjective_of_surjective đ 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) (hf : Function.Surjective (QuotientAddGroup.mk â âf)) (h : N ⤠AddSubgroup.comap f M) : Function.Surjective â(QuotientAddGroup.map N M f h) - QuotientAddGroup.map_mk' đ 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) (x : G) : (QuotientAddGroup.map N M f h) ((QuotientAddGroup.mk' N) x) = â(f x) - QuotientAddGroup.map_comp_map đ Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G â+ H) (g : H â+ I) (hf : N ⤠AddSubgroup.comap f M) (hg : M ⤠AddSubgroup.comap g O) (hgf : N ⤠AddSubgroup.comap (g.comp f) O := âŻ) : (QuotientAddGroup.map M O g hg).comp (QuotientAddGroup.map N M f hf) = QuotientAddGroup.map N O (g.comp f) hgf - QuotientAddGroup.map_map đ Mathlib.GroupTheory.QuotientGroup.Defs
{G : Type u} [AddGroup G] (N : AddSubgroup G) [nN : N.Normal] {H : Type v} [AddGroup H] {I : Type u_1} [AddGroup I] (M : AddSubgroup H) (O : AddSubgroup I) [M.Normal] [O.Normal] (f : G â+ H) (g : H â+ I) (hf : N ⤠AddSubgroup.comap f M) (hg : M ⤠AddSubgroup.comap g O) (hgf : N ⤠AddSubgroup.comap (g.comp f) O := âŻ) (x : G ⧸ N) : (QuotientAddGroup.map M O g hg) ((QuotientAddGroup.map N M f hf) x) = (QuotientAddGroup.map N O (g.comp f) hgf) x - 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.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.quotientMapAddSubgroupOfOfLe.eq_1 đ Mathlib.GroupTheory.QuotientGroup.Basic
{G : Type u} [AddGroup G] {A' A B' B : AddSubgroup G} [_hAN : (A'.addSubgroupOf A).Normal] [_hBN : (B'.addSubgroupOf B).Normal] (h' : A' ⤠B') (h : A ⤠B) : QuotientAddGroup.quotientMapAddSubgroupOfOfLe h' h = QuotientAddGroup.map (A'.addSubgroupOf A) (B'.addSubgroupOf B) (AddSubgroup.inclusion h) ⯠- 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 đ 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
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 findtsum_lt_tsum
even though the hypothesisf 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 ee8c038
serving mathlib revision 7a9e177