Documentation Verification Report

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.sum` `TensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `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.sum` `TensorProduct` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `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` `zero`	`Finsupp` `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` `zero`	`Finsupp` `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