Loogle!

Result

Found 15 declarations mentioning IsTensorProduct.map.

• IsTensorProduct.map_id 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) : hf.map hf LinearMap.id LinearMap.id = LinearMap.id
• IsTensorProduct.map_one 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) : hf.map hf 1 1 = 1
• IsTensorProduct.map 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) : M →ₗ[R] N
• IsTensorProduct.map_pow 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) (i : M₁ →ₗ[R] M₁) (j : M₂ →ₗ[R] M₂) (n : ℕ) : hf.map hf i j ^ n = hf.map hf (i ^ n) (j ^ n)
• IsTensorProduct.map_mul 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) (i₁ i₂ : M₁ →ₗ[R] M₁) (j₁ j₂ : M₂ →ₗ[R] M₂) : hf.map hf (i₁ * i₂) (j₁ * j₂) = hf.map hf i₁ j₁ * hf.map hf i₂ j₂
• IsTensorProduct.map.eq_1 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) : hf.map hg i₁ i₂ = ↑hg.equiv ∘ₗ TensorProduct.map i₁ i₂ ∘ₗ ↑hf.equiv.symm
• IsTensorProduct.map_comp 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} {P₁ : Type u_9} {P₂ : Type u_10} {P : Type u_11} [AddCommMonoid P₁] [AddCommMonoid P₂] [AddCommMonoid P] [Module R P₁] [Module R P₂] [Module R P] {p : P₁ →ₗ[R] P₂ →ₗ[R] P} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (hp : IsTensorProduct p) (i₁ : N₁ →ₗ[R] P₁) (j₁ : M₁ →ₗ[R] N₁) (i₂ : N₂ →ₗ[R] P₂) (j₂ : M₂ →ₗ[R] N₂) : hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) = hg.map hp i₁ i₂ ∘ₗ hf.map hg j₁ j₂
• IsTensorProduct.map_map 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} {P₁ : Type u_9} {P₂ : Type u_10} {P : Type u_11} [AddCommMonoid P₁] [AddCommMonoid P₂] [AddCommMonoid P] [Module R P₁] [Module R P₂] [Module R P] {p : P₁ →ₗ[R] P₂ →ₗ[R] P} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (hp : IsTensorProduct p) (i₁ : N₁ →ₗ[R] P₁) (j₁ : M₁ →ₗ[R] N₁) (i₂ : N₂ →ₗ[R] P₂) (j₂ : M₂ →ₗ[R] N₂) (x : M) : (hg.map hp i₁ i₂) ((hf.map hg j₁ j₂) x) = (hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂)) x
• IsTensorProduct.map_eq 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (x₁ : M₁) (x₂ : M₂) : (hf.map hg i₁ i₂) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)
• IsTensorProduct.map.congr_simp 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} [CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M] [Module R M₁] [Module R M₂] [Module R M] {f f✝ : M₁ →ₗ[R] M₂ →ₗ[R] M} (e_f : f = f✝) {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8} [AddCommMonoid N₁] [AddCommMonoid N₂] [AddCommMonoid N] [Module R N₁] [Module R N₂] [Module R N] {g g✝ : N₁ →ₗ[R] N₂ →ₗ[R] N} (e_g : g = g✝) (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ i₁✝ : M₁ →ₗ[R] N₁) (e_i₁ : i₁ = i₁✝) (i₂ i₂✝ : M₂ →ₗ[R] N₂) (e_i₂ : i₂ = i₂✝) : hf.map hg i₁ i₂ = ⋯.map ⋯ i₁✝ i₂✝
• IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap 📋 Mathlib.RingTheory.IsTensorProduct
  {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [AddCommMonoid M] [AddCommMonoid N] [CommSemiring R] [CommSemiring S] [Algebra R S] [Module R M] [Module R N] [Module S N] [IsScalarTower R S N] {f : M →ₗ[R] N} (hf : IsBaseChange S f) (x : R) : IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x) = ↑R ((LinearMap.lsmul S N) ((algebraMap R S) x))
• IsTensorProduct.map_id_injective_of_flat_left 📋 Mathlib.RingTheory.Flat.Basic
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_8} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [AddCommMonoid N₂] [Module R N₂] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) {g : M₁ →ₗ[R] N₂ →ₗ[R] N} (hg : IsTensorProduct g) (i : M₂ →ₗ[R] N₂) (hi : Function.Injective ⇑i) [Module.Flat R M₁] : Function.Injective ⇑(hf.map hg LinearMap.id i)
• IsTensorProduct.map_id_injective_of_flat_right 📋 Mathlib.RingTheory.Flat.Basic
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₁ : Type u_7} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [AddCommMonoid N₁] [Module R N₁] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (hf : IsTensorProduct f) {g : N₁ →ₗ[R] M₂ →ₗ[R] N} (hg : IsTensorProduct g) (i : M₁ →ₗ[R] N₁) (hi : Function.Injective ⇑i) [Module.Flat R M₂] : Function.Injective ⇑(hf.map hg i LinearMap.id)
• IsTensorProduct.map_injective_of_flat_left_right 📋 Mathlib.RingTheory.Flat.Basic
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₁ : Type u_7} {N₂ : Type u_8} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (h₁ : Function.Injective ⇑i₁) (h₂ : Function.Injective ⇑i₂) [Module.Flat R M₁] [Module.Flat R N₂] : Function.Injective ⇑(hf.map hg i₁ i₂)
• IsTensorProduct.map_injective_of_flat_right_left 📋 Mathlib.RingTheory.Flat.Basic
  {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {M₁ : Type u_5} {M₂ : Type u_6} {N₁ : Type u_7} {N₂ : Type u_8} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [AddCommMonoid N₁] [AddCommMonoid N₂] [Module R N₁] [Module R N₂] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (h₁ : Function.Injective ⇑i₁) (h₂ : Function.Injective ⇑i₂) [Module.Flat R M₂] [Module.Flat R N₁] : Function.Injective ⇑(hf.map hg i₁ i₂)

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 ee8c038 serving mathlib revision 7a9e177