Loogle!

Result

Found 47 declarations mentioning Sym2.map.

• Sym2.map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} (f : α → β) : Sym2 α → Sym2 β
• Sym2.map_id 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} : Sym2.map id = id
• Sym2.map_id' 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} : (Sym2.map fun x => x) = id
• Sym2.IsDiag.map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {e : Sym2 α} {f : α → β} : e.IsDiag → (Sym2.map f e).IsDiag
• Sym2.map.injective 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {f : α → β} (hinj : Function.Injective f) : Function.Injective (Sym2.map f)
• Sym2.isDiag_map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {e : Sym2 α} {f : α → β} (hf : Function.Injective f) : (Sym2.map f e).IsDiag ↔ e.IsDiag
• Sym2.map_pair_eq 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} (f : α → β) (x y : α) : Sym2.map f s(x, y) = s(f x, f y)
• Sym2.map_map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} (x : Sym2 α) : Sym2.map g (Sym2.map f x) = Sym2.map (g ∘ f) x
• Sym2.map_comp 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β → γ} {f : α → β} : Sym2.map (g ∘ f) = Sym2.map g ∘ Sym2.map f
• Sym2.map_congr 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {f g : α → β} {s : Sym2 α} (h : ∀ x ∈ s, f x = g x) : Sym2.map f s = Sym2.map g s
• Sym2.attachWith_map_subtypeVal 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {s : Sym2 α} {P : α → Prop} (h : ∀ a ∈ s, P a) : Sym2.map Subtype.val (s.attachWith h) = s
• Sym2.pmap_eq_map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : α → β) (z : Sym2 α) (h : ∀ a ∈ z, P a) : Sym2.pmap (fun a x => f a) z h = Sym2.map f z
• Sym2.fromRel_relationMap 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (hr : Symmetric r) (f : α → β) : Sym2.fromRel ⋯ = Sym2.map f '' Sym2.fromRel hr
• Sym2.pmap_subtype_map_subtypeVal 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {P : α → Prop} (s : Sym2 α) (h : ∀ a ∈ s, P a) : Sym2.map Subtype.val (Sym2.pmap Subtype.mk s h) = s
• Sym2.mem_map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {z : Sym2 α} : b ∈ Sym2.map f z ↔ ∃ a ∈ z, f a = b
• Function.Embedding.sym2Map_apply 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a✝ : Sym2 α) : f.sym2Map a✝ = Sym2.map (⇑f) a✝
• Sym2.pmap_map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {P : α → Prop} {Q : β → Prop} (f : (a : α) → P a → β) (g : β → γ) (z : Sym2 α) (h : ∀ a ∈ z, P a) (h' : ∀ b ∈ Sym2.pmap f z h, Q b) : Sym2.map g (Sym2.pmap f z h) = Sym2.pmap (fun a ha => g (f a ⋯)) z ⋯
• Sym2.map_pmap 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {Q : β → Prop} (f : α → β) (g : (b : β) → Q b → γ) (z : Sym2 α) (h : ∀ b ∈ Sym2.map f z, Q b) : Sym2.pmap g (Sym2.map f z) h = Sym2.pmap (fun a ha => g (f a) ⋯) z ⋯
• Sym2.lift_map_apply 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ → α} (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (p : Sym2 γ) : Sym2.lift f (Sym2.map g p) = Sym2.lift ⟨fun c₁ c₂ => ↑f (g c₁) (g c₂), ⋯⟩ p
• Sym2.lift_comp_map 📋 Mathlib.Data.Sym.Sym2
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ → α} (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) : Sym2.lift f ∘ Sym2.map g = Sym2.lift ⟨fun c₁ c₂ => ↑f (g c₁) (g c₂), ⋯⟩
• List.sym2_map 📋 Mathlib.Data.List.Sym
  {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α) : (List.map f xs).sym2 = List.map (Sym2.map f) xs.sym2
• Multiset.sym2_map 📋 Mathlib.Data.Multiset.Sym
  {α : Type u_1} {β : Type u_2} (f : α → β) (m : Multiset α) : (Multiset.map f m).sym2 = Multiset.map (Sym2.map f) m.sym2
• Finset.sym2_image 📋 Mathlib.Data.Finset.Sym
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) : (Finset.image f s).sym2 = Finset.image (Sym2.map f) s.sym2
• QuadraticMap.map_sum' 📋 Mathlib.LinearAlgebra.QuadraticForm.Basic
  {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_8} (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M) : Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, QuadraticMap.polarSym2 (⇑Q) (Sym2.map f ij) - ∑ i ∈ s, Q (f i)
• QuadraticMap.map_sum 📋 Mathlib.LinearAlgebra.QuadraticForm.Basic
  {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_8} [DecidableEq ι] (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M) : Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, QuadraticMap.polarSym2 (⇑Q) (Sym2.map f ij)
• QuadraticMap.polarSym2_map_smul 📋 Mathlib.LinearAlgebra.QuadraticForm.Basic
  {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {ι : Type u_8} (Q : QuadraticMap R M N) (g : ι → M) (l : ι → R) (p : Sym2 ι) : QuadraticMap.polarSym2 (⇑Q) (Sym2.map (l • g) p) = (Sym2.map l p).mul • QuadraticMap.polarSym2 (⇑Q) (Sym2.map g p)
• SimpleGraph.Hom.map_mem_edgeSet 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') {e : Sym2 V} (h : e ∈ G.edgeSet) : Sym2.map (⇑f) e ∈ G'.edgeSet
• SimpleGraph.Embedding.map_mem_edgeSet_iff 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {e : Sym2 V} : Sym2.map (⇑f) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet
• SimpleGraph.Iso.map_mem_edgeSet_iff 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') {e : Sym2 V} : Sym2.map (⇑f) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet
• SimpleGraph.Hom.mapEdgeSet_coe 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑G.edgeSet) : ↑(f.mapEdgeSet e) = Sym2.map ⇑f ↑e
• SimpleGraph.Hom.mapEdgeSet.eq_1 📋 Mathlib.Combinatorics.SimpleGraph.Maps
  {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (e : ↑G.edgeSet) : f.mapEdgeSet e = ⟨Sym2.map ⇑f ↑e, ⋯⟩
• SimpleGraph.Walk.edgeSet_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).edgeSet = Sym2.map ⇑f '' p.edgeSet
• SimpleGraph.Walk.edges_map 📋 Mathlib.Combinatorics.SimpleGraph.Walk
  {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges
• SimpleGraph.Subgraph.image_coe_edgeSet_coe 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
  {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) : Sym2.map Subtype.val '' G'.coe.edgeSet = G'.edgeSet
• SimpleGraph.Subgraph.edgeSet_map 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
  {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph) : (SimpleGraph.Subgraph.map f H).edgeSet = Sym2.map ⇑f '' H.edgeSet
• SimpleGraph.Subgraph.edgeSet_coe 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
  {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} : G'.coe.edgeSet = Sym2.map Subtype.val ⁻¹' G'.edgeSet
• SimpleGraph.Subgraph.coe_deleteEdges_eq 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
  {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 V)) : (G'.deleteEdges s).coe = G'.coe.deleteEdges (Sym2.map Subtype.val ⁻¹' s)
• SimpleGraph.Subgraph.deleteEdges_coe_eq 📋 Mathlib.Combinatorics.SimpleGraph.Subgraph
  {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (s : Set (Sym2 ↑G'.verts)) : G'.coe.deleteEdges s = (G'.deleteEdges (Sym2.map Subtype.val '' s)).coe
• Finsupp.mem_sym2_support_of_mul_ne_zero 📋 Mathlib.Data.Sym.Sym2.Finsupp
  {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] {f : α →₀ M₀} (p : Sym2 α) (hp : (Sym2.map (⇑f) p).mul ≠ 0) : p ∈ f.support.sym2
• Finsupp.coe_sym2Mul 📋 Mathlib.Data.Sym.Sym2.Finsupp
  {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] (f : α →₀ M₀) : ⇑f.sym2Mul = Sym2.mul ∘ Sym2.map ⇑f
• Finsupp.sym2_support_eq_preimage_support_mul 📋 Mathlib.Data.Sym.Sym2.Finsupp
  {α : Type u_1} {M₀ : Type u_2} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] (f : α →₀ M₀) : ↑f.support.sym2 = Sym2.map ⇑f ⁻¹' Function.support Sym2.mul
• QuadraticMap.map_finsuppSum' 📋 Mathlib.LinearAlgebra.QuadraticForm.Basis
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (f : ι →₀ R) (g : ι → R → M) : Q (f.sum g) = ∑ p ∈ f.support.sym2, QuadraticMap.polarSym2 (⇑Q) (Sym2.map (fun i => g i (f i)) p) - f.sum fun i a => Q (g i a)
• QuadraticMap.map_finsuppSum 📋 Mathlib.LinearAlgebra.QuadraticForm.Basis
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] (Q : QuadraticMap R M N) (f : ι →₀ R) (g : ι → R → M) : Q (f.sum g) = (f.sum fun i r => Q (g i r)) + ∑ p ∈ f.support.sym2 with ¬p.IsDiag, QuadraticMap.polarSym2 (⇑Q) (Sym2.map (fun i => g i (f i)) p)
• QuadraticMap.apply_linearCombination 📋 Mathlib.LinearAlgebra.QuadraticForm.Basis
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] (Q : QuadraticMap R M N) {g : ι → M} (l : ι →₀ R) : Q ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (⇑Q ∘ g)) (l * l) + ∑ p ∈ l.support.sym2 with ¬p.IsDiag, (Sym2.map (⇑l) p).mul • QuadraticMap.polarSym2 (⇑Q) (Sym2.map g p)
• QuadraticMap.apply_linearCombination' 📋 Mathlib.LinearAlgebra.QuadraticForm.Basis
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) {g : ι → M} (l : ι →₀ R) : Q ((Finsupp.linearCombination R g) l) = (Finsupp.linearCombination R (QuadraticMap.polarSym2 ⇑Q ∘ Sym2.map g)) l.sym2Mul - (Finsupp.linearCombination R (⇑Q ∘ g)) (l * l)
• QuadraticMap.sum_polar_sub_repr_sq 📋 Mathlib.LinearAlgebra.QuadraticForm.Basis
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (bm : Basis ι R M) (x : M) : (Finsupp.linearCombination R (QuadraticMap.polarSym2 ⇑Q ∘ Sym2.map ⇑bm)) (bm.repr x).sym2Mul - (Finsupp.linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) = Q x
• QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar 📋 Mathlib.LinearAlgebra.QuadraticForm.Basis
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] (Q : QuadraticMap R M N) (bm : Basis ι R M) (x : M) : (Finsupp.linearCombination R (⇑Q ∘ ⇑bm)) (bm.repr x * bm.repr x) + ∑ p ∈ (bm.repr x).support.sym2 with ¬p.IsDiag, (Sym2.map (⇑(bm.repr x)) p).mul • QuadraticMap.polarSym2 (⇑Q) (Sym2.map (⇑bm) p) = Q 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:

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