Loogle!
Result
Found 15 declarations mentioning AddSubmonoid.LocalizationMap.map.
- AddSubmonoid.LocalizationMap.map 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] (k : T.LocalizationMap Q) : N →+ Q - AddSubmonoid.LocalizationMap.map.eq_1 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] (k : T.LocalizationMap Q) : f.map hy k = f.lift ⋯ - AddSubmonoid.LocalizationMap.map_comp 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} : (f.map hy k).comp f.toMap = k.toMap.comp g - AddSubmonoid.LocalizationMap.map_injective_of_injective 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {Q : Type u_4} [AddCommMonoid Q] (hg : Function.Injective ⇑g) (k : (AddSubmonoid.map g S).LocalizationMap Q) : Function.Injective ⇑(f.map ⋯ k) - AddSubmonoid.LocalizationMap.map_surjective_of_surjective 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {Q : Type u_4} [AddCommMonoid Q] (hg : Function.Surjective ⇑g) (k : (AddSubmonoid.map g S).LocalizationMap Q) : Function.Surjective ⇑(f.map ⋯ k) - AddSubmonoid.LocalizationMap.map_eq 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (x : M) : (f.map hy k) (f.toMap x) = k.toMap (g x) - AddSubmonoid.LocalizationMap.map_mk' 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (x : M) (y : ↥S) : (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩ - AddSubmonoid.LocalizationMap.map_add_left 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) : k.toMap (g ↑(f.sec z).2) + (f.map hy k) z = k.toMap (g (f.sec z).1) - AddSubmonoid.LocalizationMap.map_add_right 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) : (f.map hy k) z + k.toMap (g ↑(f.sec z).2) = k.toMap (g (f.sec z).1) - AddSubmonoid.LocalizationMap.map_spec 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) (u : Q) : (f.map hy k) z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g ↑(f.sec z).2) + u - AddSubmonoid.LocalizationMap.map_id 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] (f : S.LocalizationMap N) (z : N) : (f.map ⋯ f) z = z - AddSubmonoid.LocalizationMap.map_comp_map 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_6} [AddCommMonoid R] (j : U.LocalizationMap R) {l : P →+ A} (hl : ∀ (w : ↥T), l ↑w ∈ U) : (k.map hl j).comp (f.map hy k) = f.map ⋯ j - AddSubmonoid.LocalizationMap.map_map 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_6} [AddCommMonoid R] (j : U.LocalizationMap R) {l : P →+ A} (hl : ∀ (w : ↥T), l ↑w ∈ U) (x : N) : (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x - AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) : (f.addEquivOfAddEquiv k H).toAddMonoidHom = f.map ⋯ k - AddSubmonoid.LocalizationMap.addEquivOfAddEquiv_eq_map_apply 📋 Mathlib.GroupTheory.MonoidLocalization.Basic
{M : Type u_1} [AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [AddCommMonoid N] {P : Type u_3} [AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [AddCommMonoid Q] {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : N) : (f.addEquivOfAddEquiv k H) x = (f.map ⋯ k) 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 19971e9
serving mathlib revision bce1d65