Loogle!

Result

Found 49 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 : Basis ι R M) (c : 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 : Basis ι R M) (c : 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.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 : Basis ι R M) (c : 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 = (↑(TensorProduct.lid R R)).compRight ∘ₗ 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 : Basis ι R M) (c : 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 : Basis ι R M) (c : 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_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 : Basis ι R M) (c : 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.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 : Basis ι R M) (c : 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.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 : Basis ι R M) (c : 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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : 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) [CommRing R] [AddCommGroup M] [AddCommGroup 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
• dualTensorHomEquiv.eq_1 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) (N : Type u_4) [CommRing R] [AddCommGroup M] [AddCommGroup 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)
• 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
• dualTensorHomEquivOfBasis_toLinearMap 📋 Mathlib.LinearAlgebra.Contraction
  {ι : 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 ι] [Fintype ι] (b : Basis ι R M) : ↑(dualTensorHomEquivOfBasis b) = dualTensorHom R M N
• 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 : Basis m R M) (bN : 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
• 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)
• lTensorHomEquivHomLTensor.eq_1 📋 Mathlib.LinearAlgebra.Contraction
  (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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) [CommRing R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup 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))
• 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)
• dualTensorHomEquivOfBasis_apply 📋 Mathlib.LinearAlgebra.Contraction
  {ι : 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 ι] [Fintype ι] (b : Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) : (dualTensorHomEquivOfBasis b) x = (dualTensorHom R M N) x
• dualTensorHomEquivOfBasis_symm_cancel_right 📋 Mathlib.LinearAlgebra.Contraction
  {ι : 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 ι] [Fintype ι] (b : 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} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [DecidableEq ι] [Fintype ι] (b : Basis ι R M) (x : TensorProduct R (Module.Dual R M) N) : (dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x
• 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_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 = let bV := 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 = ((Basis.singleton Unit K).constr K) fun x => ∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (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 : 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 : 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)

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 e0654b0