CanonicalTensor

📁 Source: Mathlib/Analysis/InnerProductSpace/CanonicalTensor.lean

Statistics

Metric	Count
Definitions canonicalContravariantTensor, canonicalCovariantTensor	2
Theorems canonicalCovariantTensor_eq_sum	1
Total	3

InnerProductSpace

Definitions

Name	Category	Theorems
canonicalContravariantTensor 📖	CompOp	—
canonicalCovariantTensor 📖	CompOp	2 math math: canonicalCovariantTensor_eq_sum, LineDeriv.tensorLineDerivTwo_canonicalCovariantTensor_eq_sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonicalCovariantTensor_eq_sum 📖	mathematical	—	canonicalCovariantTensor Finset.sum TensorProduct Real Real.instCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField toNormedSpace Real.instRCLike TensorProduct.addCommMonoid Finset.univ TensorProduct.tmul DFunLike.coe OrthonormalBasis OrthonormalBasis.instFunLike	—	Fintype.sum_eq_single orthonormal_iff_ite OrthonormalBasis.orthonormal ite_smul one_smul zero_smul Finset.sum_congr OrthonormalBasis.sum_inner_mul_inner real_inner_comm Finset.sum_smul TensorProduct.tmul_sum TensorProduct.sum_tmul TensorProduct.smul_tmul_smul Finset.sum_comm OrthonormalBasis.sum_repr'

---

← Back to Index