Loogle!

Result

Found 19 declarations mentioning TensorProduct.AlgebraTensorModule.map.

• TensorProduct.AlgebraTensorModule.map_id 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : TensorProduct.AlgebraTensorModule.map LinearMap.id LinearMap.id = LinearMap.id
• TensorProduct.AlgebraTensorModule.map 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct R M N →ₗ[A] TensorProduct R P Q
• TensorProduct.AlgebraTensorModule.map_one 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] : TensorProduct.AlgebraTensorModule.map 1 1 = 1
• TensorProduct.AlgebraTensorModule.map_tmul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : (TensorProduct.AlgebraTensorModule.map f g) (m ⊗ₜ[R] n) = f m ⊗ₜ[R] g n
• TensorProduct.AlgebraTensorModule.map_comp 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [AddCommMonoid P'] [Module R P'] [Module A P'] [IsScalarTower R A P'] [AddCommMonoid Q'] [Module R Q'] (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) = TensorProduct.AlgebraTensorModule.map f₂ g₂ ∘ₗ TensorProduct.AlgebraTensorModule.map f₁ g₁
• TensorProduct.AlgebraTensorModule.map_mul 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] (f₁ f₂ : M →ₗ[A] M) (g₁ g₂ : N →ₗ[R] N) : TensorProduct.AlgebraTensorModule.map (f₁ * f₂) (g₁ * g₂) = TensorProduct.AlgebraTensorModule.map f₁ g₁ * TensorProduct.AlgebraTensorModule.map f₂ g₂
• TensorProduct.AlgebraTensorModule.map_add_left 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (f₁ + f₂) g = TensorProduct.AlgebraTensorModule.map f₁ g + TensorProduct.AlgebraTensorModule.map f₂ g
• TensorProduct.AlgebraTensorModule.map_smul_right 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f (r • g) = r • TensorProduct.AlgebraTensorModule.map f g
• TensorProduct.AlgebraTensorModule.map_add_right 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map f (g₁ + g₂) = TensorProduct.AlgebraTensorModule.map f g₁ + TensorProduct.AlgebraTensorModule.map f g₂
• TensorProduct.AlgebraTensorModule.map_smul_left 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : TensorProduct.AlgebraTensorModule.map (b • f) g = b • TensorProduct.AlgebraTensorModule.map f g
• TensorProduct.AlgebraTensorModule.homTensorHomMap_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : (TensorProduct.AlgebraTensorModule.homTensorHomMap R A B M N P Q) (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
• TensorProduct.AlgebraTensorModule.rTensor_tensor 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  (R : Type uR) (A : Type uA) {M : Type uM} {N : Type uN} {P : Type uP} (P' : Type uP') [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module A P] [AddCommMonoid P'] [Module A P'] [Module R P] [IsScalarTower R A P] [Module R P'] [IsScalarTower R A P'] (g : P →ₗ[A] P') : LinearMap.rTensor (TensorProduct R M N) g = ↑(TensorProduct.AlgebraTensorModule.assoc R A A P' M N) ∘ₗ TensorProduct.AlgebraTensorModule.map (LinearMap.rTensor M g) LinearMap.id ∘ₗ ↑(TensorProduct.AlgebraTensorModule.assoc R A A P M N).symm
• TensorProduct.AlgebraTensorModule.mapBilinear_apply 📋 Mathlib.LinearAlgebra.TensorProduct.Tower
  {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] [AddCommMonoid N] [Module R N] [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] [AddCommMonoid Q] [Module R Q] [Module B P] [IsScalarTower R B P] [SMulCommClass A B P] (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : ((TensorProduct.AlgebraTensorModule.mapBilinear R A B M N P Q) f) g = TensorProduct.AlgebraTensorModule.map f g
• TensorProduct.directSum.eq_1 📋 Mathlib.LinearAlgebra.DirectSum.TensorProduct
  (R : Type u) [CommSemiring R] (S : Type u_1) [Semiring S] [Algebra R S] {ι₁ : Type v₁} {ι₂ : Type v₂} [DecidableEq ι₁] [DecidableEq ι₂] (M₁ : ι₁ → Type w₁) (M₂ : ι₂ → Type w₂) [(i₁ : ι₁) → AddCommMonoid (M₁ i₁)] [(i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [(i₁ : ι₁) → Module R (M₁ i₁)] [(i₂ : ι₂) → Module R (M₂ i₂)] [(i₁ : ι₁) → Module S (M₁ i₁)] [∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] : TensorProduct.directSum R S M₁ M₂ = LinearEquiv.ofLinear (TensorProduct.AlgebraTensorModule.lift (DirectSum.toModule S ι₁ ((DirectSum ι₂ fun i₂ => M₂ i₂) →ₗ[R] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) fun i₁ => (DirectSum.toModule R ι₂ (M₁ i₁ →ₗ[S] DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) fun i₂ => (TensorProduct.AlgebraTensorModule.curry (DirectSum.lof S (ι₁ × ι₂) (fun i => TensorProduct R (M₁ i.1) (M₂ i.2)) (i₁, i₂))).flip).flip)) (DirectSum.toModule S (ι₁ × ι₂) (TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) (DirectSum ι₂ fun i₂ => M₂ i₂)) fun i => TensorProduct.AlgebraTensorModule.map (DirectSum.lof S ι₁ M₁ i.1) (DirectSum.lof R ι₂ M₂ i.2)) ⋯ ⋯
• Module.endTensorEndAlgHom_apply 📋 Mathlib.RingTheory.TensorProduct.Basic
  {R : Type u_1} {S : Type u_2} {A : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [CommSemiring S] [Semiring A] [AddCommMonoid M] [AddCommMonoid N] [Algebra R S] [Algebra S A] [Algebra R A] [Module R M] [Module S M] [Module A M] [Module R N] [IsScalarTower R A M] [IsScalarTower S A M] [IsScalarTower R S M] (f : Module.End A M) (g : Module.End R N) : Module.endTensorEndAlgHom (f ⊗ₜ[R] g) = TensorProduct.AlgebraTensorModule.map f g
• isBaseChange_tensorProduct_map 📋 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] {P : Type u_2} [AddCommMonoid P] [Module R P] (A : Type u_4) [CommSemiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Module S M] [IsScalarTower R S M] [Module A N] [IsScalarTower S A N] [IsScalarTower R A N] {f : M →ₗ[S] N} (hf : IsBaseChange A f) : IsBaseChange A (TensorProduct.AlgebraTensorModule.map f LinearMap.id)
• AdicCompletion.tensor_map_id_left_injective_of_injective 📋 Mathlib.RingTheory.AdicCompletion.AsTensorProduct
  {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} [Module.Finite R M] [Module.Finite R N] (hf : Function.Injective ⇑f) : Function.Injective ⇑(TensorProduct.AlgebraTensorModule.map LinearMap.id f)
• AdicCompletion.ofTensorProduct_naturality 📋 Mathlib.RingTheory.AdicCompletion.AsTensorProduct
  {R : Type u_1} [CommRing R] (I : Ideal R) {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : AdicCompletion.map I f ∘ₗ AdicCompletion.ofTensorProduct I M = AdicCompletion.ofTensorProduct I N ∘ₗ TensorProduct.AlgebraTensorModule.map LinearMap.id f
• AdicCompletion.tensor_map_id_left_eq_map 📋 Mathlib.RingTheory.AdicCompletion.AsTensorProduct
  {R : Type u} [CommRing R] (I : Ideal R) [IsNoetherianRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) [Module.Finite R M] [Module.Finite R N] : TensorProduct.AlgebraTensorModule.map LinearMap.id f = ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I N).symm ∘ₗ AdicCompletion.map I f ∘ₗ ↑(AdicCompletion.ofTensorProductEquivOfFiniteNoetherian I M)

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