Basis

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

Statistics

Metric	Count
Definitions baseChange, tensorProduct, equivFinsuppOfBasisLeft, equivFinsuppOfBasisRight	4
Theorems baseChange_apply, baseChange_repr_tmul, tensorProduct_apply, tensorProduct_apply', tensorProduct_repr_tmul_apply, tensor, eq_repr_basis_left, eq_repr_basis_right, equivFinsuppOfBasisLeft_apply, equivFinsuppOfBasisLeft_apply_tmul, equivFinsuppOfBasisLeft_apply_tmul_apply, equivFinsuppOfBasisLeft_symm, equivFinsuppOfBasisLeft_symm_apply, equivFinsuppOfBasisRight_apply, equivFinsuppOfBasisRight_apply_tmul, equivFinsuppOfBasisRight_apply_tmul_apply, equivFinsuppOfBasisRight_symm, equivFinsuppOfBasisRight_symm_apply, sum_tmul_basis_left_eq_zero, sum_tmul_basis_left_injective, sum_tmul_basis_right_eq_zero, sum_tmul_basis_right_injective	22
Total	26

Module.Basis

Definitions

Name	Category	Theorems
baseChange 📖	CompOp	2 math math: baseChange_apply, baseChange_repr_tmul
tensorProduct 📖	CompOp	9 math math: Matrix.toLin_kronecker, tensorProduct_apply, OrthonormalBasis.toBasis_tensorProduct, Orthonormal.basisTensorProduct, TensorProduct.toMatrix_assoc, tensorProduct_apply', tensorProduct_repr_tmul_apply, TensorProduct.toMatrix_comm, TensorProduct.toMatrix_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_apply 📖	mathematical	—	DFunLike.coe Module.Basis TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule TensorProduct.addCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass instFunLike baseChange TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne CommSemiring.toSemiring	—	Algebra.to_smulCommClass IsScalarTower.to_smulCommClass IsScalarTower.right RingHomInvPair.ids LinearEquiv.trans.congr_simp Finsupp.lcongr_symm coe_reindex Finsupp.coe_basisSingleOne Finsupp.lcongr_single finsuppTensorFinsupp_symm_single repr_symm_apply coe_singleton Finsupp.linearCombination_single mul_one one_smul
baseChange_repr_tmul 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule TensorProduct.addCommMonoid Finsupp.instAddCommMonoid TensorProduct.leftModule Semiring.toModule Algebra.to_smulCommClass Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr baseChange TensorProduct.tmul Algebra.toSMul CommSemiring.toSemiring	—	RingHomInvPair.ids Algebra.to_smulCommClass IsScalarTower.right IsScalarTower.to_smulCommClass LinearEquiv.trans.congr_simp Finsupp.lcongr_symm repr_reindex Finsupp.smulCommClass LinearEquiv.trans_refl Finsupp.mapDomain_equiv_apply finsuppTensorFinsupp_apply singleton_repr
tensorProduct_apply 📖	mathematical	—	DFunLike.coe Module.Basis TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass instFunLike tensorProduct TensorProduct.tmul CommSemiring.toSemiring	—	IsScalarTower.to_smulCommClass RingHomInvPair.ids IsScalarTower.right LinearEquiv.trans.congr_simp Finsupp.lcongr_symm Finsupp.coe_basisSingleOne Finsupp.lcongr_single finsuppTensorFinsupp_symm_single repr_symm_apply Finsupp.linearCombination_single one_smul
tensorProduct_apply' 📖	mathematical	—	DFunLike.coe Module.Basis TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass instFunLike tensorProduct TensorProduct.tmul CommSemiring.toSemiring	—	IsScalarTower.to_smulCommClass RingHomInvPair.ids IsScalarTower.right LinearEquiv.trans.congr_simp Finsupp.lcongr_symm Finsupp.coe_basisSingleOne Finsupp.lcongr_single finsuppTensorFinsupp_symm_single repr_symm_apply Finsupp.linearCombination_single one_smul
tensorProduct_repr_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids TensorProduct TensorProduct.addCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv repr tensorProduct TensorProduct.tmul Algebra.toSMul CommSemiring.toSemiring	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.right LinearEquiv.trans.congr_simp Finsupp.lcongr_symm Finsupp.smulCommClass LinearEquiv.trans_refl finsuppTensorFinsupp_apply

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tensor 📖	mathematical	—	Module.Free TensorProduct TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass	—	IsScalarTower.to_smulCommClass exists_basis of_basis

TensorProduct

Definitions

Name	Category	Theorems
equivFinsuppOfBasisLeft 📖	CompOp	5 math math: equivFinsuppOfBasisLeft_symm_apply, equivFinsuppOfBasisLeft_apply_tmul_apply, equivFinsuppOfBasisLeft_apply_tmul, equivFinsuppOfBasisLeft_symm, equivFinsuppOfBasisLeft_apply
equivFinsuppOfBasisRight 📖	CompOp	5 math math: equivFinsuppOfBasisRight_apply_tmul, equivFinsuppOfBasisRight_apply_tmul_apply, equivFinsuppOfBasisRight_apply, equivFinsuppOfBasisRight_symm, equivFinsuppOfBasisRight_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_repr_basis_left 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.sum TensorProduct addCommMonoid tmul DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike	—	RingHomInvPair.ids LinearEquiv.surjective LinearEquiv.injective Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass equivFinsuppOfBasisLeft_symm_apply
eq_repr_basis_right 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.sum TensorProduct addCommMonoid tmul DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike	—	RingHomInvPair.ids equivFinsuppOfBasisRight_symm_apply LinearEquiv.surjective
equivFinsuppOfBasisLeft_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid Finsupp.instAddCommMonoid instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivFinsuppOfBasisLeft NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule lid LinearMap LinearMap.instFunLike LinearMap.rTensor Module.Basis.coord	—	induction_on RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.semilinearMapClass zero_smul equivFinsuppOfBasisLeft_apply_tmul map_add SemilinearMapClass.toAddHomClass
equivFinsuppOfBasisLeft_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid Finsupp.instAddCommMonoid instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivFinsuppOfBasisLeft tmul Finsupp.mapRange MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero Module.toMulActionWithZero zero_smul NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Module.Basis.repr	—	RingHomInvPair.ids zero_smul equivFinsuppOfBasisRight_apply_tmul
equivFinsuppOfBasisLeft_apply_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid Finsupp.instAddCommMonoid instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivFinsuppOfBasisLeft tmul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Module.Basis.repr	—	RingHomInvPair.ids zero_smul equivFinsuppOfBasisLeft_apply_tmul
equivFinsuppOfBasisLeft_symm 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct Finsupp.instAddCommMonoid addCommMonoid Finsupp.module instModule LinearEquiv.symm equivFinsuppOfBasisLeft DFunLike.coe LinearEquiv LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Finsupp.lsum LinearMap.instFunLike Module.Basis Module.Basis.instFunLike	—	Finsupp.lhom_ext' RingHomInvPair.ids smulCommClass_left smulCommClass_self LinearMap.ext RingHomCompTriple.ids equivFinsuppOfBasisRight_symm_apply Finsupp.sum_single_index zero_tmul Finsupp.lsum_comp_lsingle
equivFinsuppOfBasisLeft_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct Finsupp.instAddCommMonoid addCommMonoid Finsupp.module instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm equivFinsuppOfBasisLeft Finsupp.sum tmul Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids smulCommClass_left smulCommClass_self equivFinsuppOfBasisLeft_symm
equivFinsuppOfBasisRight_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid Finsupp.instAddCommMonoid instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivFinsuppOfBasisRight NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule rid LinearMap LinearMap.instFunLike LinearMap.lTensor Module.Basis.coord	—	induction_on RingHomInvPair.ids map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.semilinearMapClass zero_smul equivFinsuppOfBasisRight_apply_tmul map_add SemilinearMapClass.toAddHomClass
equivFinsuppOfBasisRight_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid Finsupp.instAddCommMonoid instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivFinsuppOfBasisRight tmul Finsupp.mapRange MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulActionWithZero.toSMulWithZero Semiring.toMonoidWithZero Module.toMulActionWithZero zero_smul NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Module.Basis.repr	—	Finsupp.ext RingHomInvPair.ids zero_smul finsuppScalarRight_apply_tmul_apply
equivFinsuppOfBasisRight_apply_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct addCommMonoid Finsupp.instAddCommMonoid instModule Finsupp.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv equivFinsuppOfBasisRight tmul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule Module.Basis.repr	—	RingHomInvPair.ids zero_smul equivFinsuppOfBasisRight_apply_tmul
equivFinsuppOfBasisRight_symm 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct Finsupp.instAddCommMonoid addCommMonoid Finsupp.module instModule LinearEquiv.symm equivFinsuppOfBasisRight DFunLike.coe LinearEquiv LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Finsupp.lsum SMulCommClass.symm SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul LinearMap.instFunLike LinearMap.flip Module.Basis Module.Basis.instFunLike	—	Finsupp.lhom_ext' RingHomInvPair.ids smulCommClass_left smulCommClass_self SMulCommClass.symm LinearMap.ext RingHomCompTriple.ids finsuppScalarRight_symm_apply_single Module.Basis.repr_symm_apply Finsupp.linearCombination_single one_smul Finsupp.lsum_comp_lsingle
equivFinsuppOfBasisRight_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct Finsupp.instAddCommMonoid addCommMonoid Finsupp.module instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm equivFinsuppOfBasisRight Finsupp.sum tmul Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids smulCommClass_left smulCommClass_self SMulCommClass.symm equivFinsuppOfBasisRight_symm
sum_tmul_basis_left_eq_zero 📖	mathematical	Finsupp.sum TensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid tmul DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike instZeroTensorProduct	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instZero	—	LinearEquiv.injective RingHomInvPair.ids equivFinsuppOfBasisLeft_symm_apply
sum_tmul_basis_left_injective 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid addCommMonoid Finsupp.module instModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Finsupp.lsum Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids LinearEquiv.injective smulCommClass_left smulCommClass_self equivFinsuppOfBasisLeft_symm
sum_tmul_basis_right_eq_zero 📖	mathematical	Finsupp.sum TensorProduct AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid tmul DFunLike.coe Module.Basis CommSemiring.toSemiring Module.Basis.instFunLike instZeroTensorProduct	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instZero	—	LinearEquiv.injective RingHomInvPair.ids equivFinsuppOfBasisRight_symm_apply
sum_tmul_basis_right_injective 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Finsupp.instAddCommMonoid addCommMonoid Finsupp.module instModule LinearMap.instFunLike LinearEquiv RingHomInvPair.ids Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module smulCommClass_left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Finsupp.lsum SMulCommClass.symm SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul LinearMap.flip Module.Basis Module.Basis.instFunLike	—	RingHomInvPair.ids LinearEquiv.injective smulCommClass_left smulCommClass_self SMulCommClass.symm equivFinsuppOfBasisRight_symm

---

← Back to Index