Loogle!

Result

Found 57 declarations mentioning TensorProduct and Module.Dual.

• TensorProduct.dualDistrib 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct R (Module.Dual R M) (Module.Dual R N) →ₗ[R] Module.Dual R (TensorProduct R M N)
• TensorProduct.dualDistribInvOfBasis 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : Module.Dual R (TensorProduct R M N) →ₗ[R] TensorProduct R (Module.Dual R M) (Module.Dual R N)
• TensorProduct.dualDistribEquivOfBasis 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct R M N)
• TensorProduct.dualDistribEquiv 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Free R M] [Module.Free R N] : TensorProduct R (Module.Dual R M) (Module.Dual R N) ≃ₗ[R] Module.Dual R (TensorProduct R M N)
• TensorProduct.dualDistribInvOfBasis.congr_simp 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} {inst✝ : DecidableEq ι} [DecidableEq ι] {inst✝¹ : DecidableEq κ} [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b b✝ : Module.Basis ι R M) (e_b : b = b✝) (c c✝ : Module.Basis κ R N) (e_c : c = c✝) : TensorProduct.dualDistribInvOfBasis b c = TensorProduct.dualDistribInvOfBasis b✝ c✝
• TensorProduct.dualDistribEquiv.eq_1 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Finite R M] [Module.Finite R N] [Module.Free R M] [Module.Free R N] : TensorProduct.dualDistribEquiv R M N = TensorProduct.dualDistribEquivOfBasis (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R N)
• TensorProduct.AlgebraTensorModule.dualDistrib 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module A M] [Module R N] [IsScalarTower R A M] : TensorProduct R (Module.Dual A M) (Module.Dual R N) →ₗ[A] Module.Dual A (TensorProduct R M N)
• TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : TensorProduct.dualDistrib R M N ∘ₗ TensorProduct.dualDistribInvOfBasis b c = LinearMap.id
• TensorProduct.dualDistrib.eq_1 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  (R : Type u_1) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct.dualDistrib R M N = LinearMap.compRight R ↑(TensorProduct.lid R R) ∘ₗ TensorProduct.homTensorHomMap R M N R R
• TensorProduct.dualDistrib_apply 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.Dual R M) (g : Module.Dual R N) (m : M) (n : N) : ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = f m * g n
• TensorProduct.AlgebraTensorModule.dualDistrib_apply 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} (A : Type u_2) {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module A M] [Module R N] [IsScalarTower R A M] (f : Module.Dual A M) (g : Module.Dual R N) (m : M) (n : N) : ((TensorProduct.AlgebraTensorModule.dualDistrib R A M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = g n • f m
• TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : TensorProduct.dualDistribInvOfBasis b c ∘ₗ TensorProduct.dualDistrib R M N = LinearMap.id
• TensorProduct.dualDistribInvOfBasis_apply 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (f : Module.Dual R (TensorProduct R M N)) : (TensorProduct.dualDistribInvOfBasis b c) f = ∑ i, ∑ j, f (b i ⊗ₜ[R] c j) • b.dualBasis i ⊗ₜ[R] c.dualBasis j
• TensorProduct.dualDistribEquivOfBasis_symm_apply 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (a : Module.Dual R (TensorProduct R M N)) : (TensorProduct.dualDistribEquivOfBasis b c).symm a = ∑ x, ∑ x_1, a (b x ⊗ₜ[R] c x_1) • b.coord x ⊗ₜ[R] c.coord x_1
• TensorProduct.dualDistribEquivOfBasis_apply_apply 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) (a✝ : TensorProduct R (Module.Dual R M) (Module.Dual R N)) (a✝¹ : TensorProduct R M N) : ((TensorProduct.dualDistribEquivOfBasis b c) a✝) a✝¹ = (TensorProduct.lid R R) (((TensorProduct.homTensorHomMap R M N R R) a✝) a✝¹)
• TensorProduct.dualDistribInvOfBasis.eq_1 📋 Mathlib.LinearAlgebra.Dual.Lemmas
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (b : Module.Basis ι R M) (c : Module.Basis κ R N) : TensorProduct.dualDistribInvOfBasis b c = ∑ i, ∑ j, (LinearMap.ringLmapEquivSelf R ℕ (TensorProduct R (Module.Dual R M) (Module.Dual R N))).symm (b.dualBasis i ⊗ₜ[R] c.dualBasis j) ∘ₗ LinearMap.applyₗ (c j) ∘ₗ LinearMap.applyₗ (b i) ∘ₗ TensorProduct.lcurry R M N R
• contractLeft 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct R (Module.Dual R M) M →ₗ[R] R
• contractRight 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct R M (Module.Dual R M) →ₗ[R] R
• dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] : TensorProduct R (Module.Dual R M) N →ₗ[R] M →ₗ[R] N
• dualTensorHomEquivOfBasis 📋 Mathlib.LinearAlgebra.Contraction
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) : TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N
• dualTensorHomEquiv 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Free R M] [Module.Finite R M] : TensorProduct R (Module.Dual R M) N ≃ₗ[R] M →ₗ[R] N
• dualTensorHomEquivOfBasis.congr_simp 📋 Mathlib.LinearAlgebra.Contraction
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {inst✝ : DecidableEq ι} [DecidableEq ι] [Fintype ι] (b b✝ : Module.Basis ι R M) (e_b : b = b✝) : dualTensorHomEquivOfBasis b = dualTensorHomEquivOfBasis b✝
• dualTensorHomEquiv.eq_1 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module.Free R M] [Module.Finite R M] : dualTensorHomEquiv R M N = dualTensorHomEquivOfBasis (Module.Free.chooseBasis R M)
• dualTensorHomEquivOfBasis_toLinearMap 📋 Mathlib.LinearAlgebra.Contraction
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) : ↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N
• contractLeft_apply 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) : (contractLeft R M) (f ⊗ₜ[R] m) = f m
• contractRight_apply 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) : (contractRight R M) (m ⊗ₜ[R] f) = f m
• dualTensorHom_apply 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (f : Module.Dual R M) (m : M) (n : N) : ((dualTensorHom R M N) (f ⊗ₜ[R] n)) m = f m • n
• toMatrix_dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {m : Type u_7} {n : Type u_8} [Fintype m] [Finite n] [DecidableEq m] [DecidableEq n] (bM : Module.Basis m R M) (bN : Module.Basis n R N) (j : m) (i : n) : (LinearMap.toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.single i j 1
• dualTensorHomEquivOfBasis_apply 📋 Mathlib.LinearAlgebra.Contraction
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) : (dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x
• lTensorHomEquivHomLTensor.eq_1 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] : lTensorHomEquivHomLTensor R M P Q = ((TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q).symm).trans (TensorProduct.leftComm R P (Module.Dual R M) Q)).trans (dualTensorHomEquiv R M (TensorProduct R P Q))
• rTensorHomEquivHomRTensor.eq_1 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommSemiring R] [AddCommMonoid M] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R P] [Module R Q] [Module.Free R M] [Module.Finite R M] : rTensorHomEquivHomRTensor R M P Q = ((TensorProduct.congr (dualTensorHomEquiv R M P).symm (LinearEquiv.refl R Q)).trans (TensorProduct.assoc R (Module.Dual R M) P Q)).trans (dualTensorHomEquiv R M (TensorProduct R P Q))
• dualTensorHomEquivOfBasis_symm_cancel_right 📋 Mathlib.LinearAlgebra.Contraction
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : M →ₗ[R] N) : (dualTensorHom R M N) ((dualTensorHomEquivOfBasis b).symm x) = x
• dualTensorHomEquivOfBasis_symm_cancel_left 📋 Mathlib.LinearAlgebra.Contraction
  {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) : (dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x
• dualTensorHom_prodMap_zero 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) : ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 = (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ LinearMap.fst R M N) ⊗ₜ[R] (LinearMap.inl R P Q) p)
• zero_prodMap_dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (g : Module.Dual R N) (q : Q) : LinearMap.prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ LinearMap.snd R M N) ⊗ₜ[R] (LinearMap.inr R P Q) q)
• comp_dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P) : (dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)
• map_dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} {Q : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [AddCommMonoid Q] [Module R M] [Module R N] [Module R P] [Module R Q] (f : Module.Dual R M) (p : P) (g : Module.Dual R N) (q : Q) : TensorProduct.map ((dualTensorHom R M P) (f ⊗ₜ[R] p)) ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (TensorProduct R M N) (TensorProduct R P Q)) ((TensorProduct.dualDistrib R M N) (f ⊗ₜ[R] g) ⊗ₜ[R] (p ⊗ₜ[R] q))
• transpose_dualTensorHom 📋 Mathlib.LinearAlgebra.Contraction
  {R : Type u_2} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Module.Dual R M) (m : M) : Module.Dual.transpose ((dualTensorHom R M M) (f ⊗ₜ[R] m)) = (dualTensorHom R (Module.Dual R M) (Module.Dual R M)) ((Module.Dual.eval R M) m ⊗ₜ[R] f)
• coevaluation 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : K →ₗ[K] TensorProduct K V (Module.Dual K V)
• coevaluation.congr_simp 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : coevaluation K V = coevaluation K V
• coevaluation_apply_one 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : (coevaluation K V) 1 = have bV := Module.Basis.ofVectorSpace K V; ∑ i, bV i ⊗ₜ[K] bV.coord i
• coevaluation.eq_1 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : coevaluation K V = ((Module.Basis.singleton Unit K).constr K) fun x => ∑ i, (Module.Basis.ofVectorSpace K V) i ⊗ₜ[K] (Module.Basis.ofVectorSpace K V).coord i
• contractLeft_assoc_coevaluation' 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) = ↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)
• contractLeft_assoc_coevaluation 📋 Mathlib.LinearAlgebra.Coevaluation
  (K : Type u) [Field K] (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] : LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V) = ↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V))
• FGModuleCat.FGModuleCatEvaluation_apply' 📋 Mathlib.Algebra.Category.FGModuleCat.Basic
  (K : Type u) [Field K] (V : FGModuleCat K) (f : ↑(FGModuleCat.FGModuleCatDual K V)) (x : ↑V) : (ModuleCat.Hom.hom (FGModuleCat.FGModuleCatEvaluation K V)) (f ⊗ₜ[K] x) = f.toFun x
• LinearMap.trace_eq_contract_of_basis 📋 Mathlib.LinearAlgebra.Trace
  {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_5} [Finite ι] (b : Module.Basis ι R M) : LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
• LinearMap.trace_eq_contract 📋 Mathlib.LinearAlgebra.Trace
  (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
• LinearMap.trace_eq_contract_of_basis' 📋 Mathlib.LinearAlgebra.Trace
  {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) : LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm
• LinearMap.trace_eq_contract' 📋 Mathlib.LinearAlgebra.Trace
  (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] : LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquiv R M M).symm
• LinearMap.trace_eq_contract_apply 📋 Mathlib.LinearAlgebra.Trace
  (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (x : TensorProduct R (Module.Dual R M) M) : (LinearMap.trace R M) ((dualTensorHom R M M) x) = (contractLeft R M) x
• Representation.dualTensorHom_comm 📋 Mathlib.RepresentationTheory.Basic
  {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) : dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W
• FDRep.dualTensorIsoLinHom_hom_hom 📋 Mathlib.RepresentationTheory.FDRep
  {k G V : Type u} [Field k] [Group G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρV : Representation k G V) (W : FDRep k G) : (FDRep.dualTensorIsoLinHom ρV W).hom.hom = ModuleCat.ofHom (dualTensorHom k V ↑W.V)
• Module.Invertible.linearEquivDual 📋 Mathlib.RingTheory.PicardGroup
  {R : Type u} {M : Type v} {N : Type u_1} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (e : TensorProduct R M N ≃ₗ[R] R) : M ≃ₗ[R] Module.Dual R N
• Module.Invertible.linearEquiv 📋 Mathlib.RingTheory.PicardGroup
  (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] : TensorProduct R (Module.Dual R M) M ≃ₗ[R] R
• Module.Invertible.linearEquiv.congr_simp 📋 Mathlib.RingTheory.PicardGroup
  (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Invertible R M] : Module.Invertible.linearEquiv R M = Module.Invertible.linearEquiv R M
• Module.Invertible.bijective 📋 Mathlib.RingTheory.PicardGroup
  {R : Type u} {M : Type v} {inst✝ : CommSemiring R} {inst✝¹ : AddCommMonoid M} {inst✝² : Module R M} [self : Module.Invertible R M] : Function.Bijective ⇑(contractLeft R M)
• Module.Invertible.mk 📋 Mathlib.RingTheory.PicardGroup
  {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (bijective : Function.Bijective ⇑(contractLeft R M)) : Module.Invertible R 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 06e7f72 serving mathlib revision 62eeacf