Basis

📁 Source: Mathlib/LinearAlgebra/PiTensorProduct/Basis.lean

Statistics

Metric	Count
Definitions piTensorProduct	1
Theorems piTensorProduct_apply, piTensorProduct_repr_tprod_apply	2
Total	3

Basis

Definitions

Name	Category	Theorems
piTensorProduct 📖	CompOp	2 math math: piTensorProduct_repr_tprod_apply, piTensorProduct_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
piTensorProduct_apply 📖	mathematical	—	DFunLike.coe Module.Basis PiTensorProduct CommSemiring.toSemiring PiTensorProduct.instAddCommMonoid PiTensorProduct.instModule Module.Basis.instFunLike piTensorProduct MultilinearMap MultilinearMap.instFunLikeForall PiTensorProduct.tprod	—	Module.Basis.ext_elem RingHomInvPair.ids Module.Basis.repr_self Finsupp.single_apply Finite.of_fintype piTensorProduct_repr_tprod_apply Finset.prod_congr Fintype.prod_ite_zero Finset.prod_const_one
piTensorProduct_repr_tprod_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids PiTensorProduct PiTensorProduct.instAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid PiTensorProduct.instModule Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr piTensorProduct Finite.of_fintype MultilinearMap MultilinearMap.instFunLikeForall PiTensorProduct.tprod Finset.prod CommSemiring.toCommMonoid Finset.univ	—	RingHomInvPair.ids Finite.of_fintype piTensorProduct.eq_1 Fintype.subsingleton LinearEquiv.trans.congr_simp Finsupp.lcongr_symm LinearEquiv.trans_refl PiTensorProduct.congr_tprod PiTensorProduct.ofFinsuppEquiv_apply PiTensorProduct.constantBaseRingEquiv_tprod

---

← Back to Index