Finsupp

📁 Source: Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

Statistics

Metric	Count
Definitions finsuppLeft, finsuppLeft', finsuppRight, finsuppScalarLeft, finsuppScalarRight, finsuppScalarRight', finsuppTensorFinsupp, finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid	10
Theorems linearCombination_one_tmul, coe_finsuppScalarRight', finsuppLeft'_apply, finsuppLeft_apply, finsuppLeft_apply_tmul, finsuppLeft_apply_tmul_apply, finsuppLeft_smul', finsuppLeft_symm_apply_single, finsuppRight_apply, finsuppRight_apply_tmul, finsuppRight_apply_tmul_apply, finsuppRight_symm_apply_single, finsuppRight_tmul_single, finsuppScalarLeft_apply, finsuppScalarLeft_apply_tmul, finsuppScalarLeft_apply_tmul_apply, finsuppScalarLeft_symm_apply_single, finsuppScalarRight_apply, finsuppScalarRight_apply_tmul, finsuppScalarRight_apply_tmul_apply, finsuppScalarRight_smul, finsuppScalarRight_symm_apply_single, finsuppTensorFinsupp'_apply_apply, finsuppTensorFinsupp'_single_tmul_single, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, finsuppTensorFinsupp'_symm_single_mul, finsuppTensorFinsuppLid_apply_apply, finsuppTensorFinsuppLid_self, finsuppTensorFinsuppLid_single_tmul_single, finsuppTensorFinsuppLid_symm_single_smul, finsuppTensorFinsuppRid_apply_apply, finsuppTensorFinsuppRid_self, finsuppTensorFinsuppRid_single_tmul_single, finsuppTensorFinsuppRid_symm_single_smul, finsuppTensorFinsupp_apply, finsuppTensorFinsupp_single, finsuppTensorFinsupp_symm_single	38
Total	48

Finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearCombination_one_tmul 📖	mathematical	—	LinearMap.restrictScalars Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule CommSemiring.toSemiring instAddCommMonoid TensorProduct.addCommMonoid module TensorProduct.instModule Semiring.toModule TensorProduct.leftModule Algebra.to_smulCommClass LinearMap.CompatibleSMul.finsupp_dom DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommMonoid.toAddMonoid TensorProduct.instDistribMulAction LinearMap.IsScalarTower.compatibleSMul' SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero TensorProduct.isScalarTower_left IsScalarTower.right linearCombination TensorProduct.tmul AddMonoidWithOne.toOne LinearMap.comp RingHom.id RingHomCompTriple.ids LinearMap.lTensor LinearEquiv.toLinearMap RingHomInvPair.ids IsScalarTower.to_smulCommClass Algebra.id IsScalarTower.left DistribMulAction.toMulAction LinearEquiv.symm TensorProduct.finsuppScalarRight	—	lhom_ext' Algebra.to_smulCommClass LinearMap.CompatibleSMul.finsupp_dom LinearMap.IsScalarTower.compatibleSMul' TensorProduct.isScalarTower_left IsScalarTower.right RingHomCompTriple.ids RingHomInvPair.ids IsScalarTower.to_smulCommClass IsScalarTower.left LinearMap.ext linearCombination_single mul_one TensorProduct.finsuppScalarRight_symm_apply_single one_smul

TensorProduct

Definitions

Name	Category	Theorems
finsuppLeft 📖	CompOp	8 math math: finsuppLeft_smul', finsuppLeft_symm_apply_single, finsuppLeft_apply, Rep.finsuppTensorLeft_inv_hom, Rep.finsuppTensorLeft_hom_hom, finsuppLeft_apply_tmul, finsuppLeft'_apply, finsuppLeft_apply_tmul_apply
finsuppLeft' 📖	CompOp	—
finsuppRight 📖	CompOp	7 math math: finsuppRight_apply, Rep.finsuppTensorRight_hom_hom, Rep.finsuppTensorRight_inv_hom, finsuppRight_symm_apply_single, finsuppRight_apply_tmul_apply, finsuppRight_apply_tmul, finsuppRight_tmul_single
finsuppScalarLeft 📖	CompOp	5 math math: finsuppScalarLeft_apply_tmul_apply, Submodule.mulLeftMap_eq_mulMap_comp, finsuppScalarLeft_apply_tmul, finsuppScalarLeft_apply, finsuppScalarLeft_symm_apply_single
finsuppScalarRight 📖	CompOp	10 math math: Finsupp.linearCombination_one_tmul, finsuppScalarRight_apply, finsuppScalarRight_apply_tmul, Algebra.TensorProduct.equivFinsuppOfBasis_apply, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, finsuppScalarRight_smul, finsuppScalarRight_apply_tmul_apply, Submodule.mulRightMap_eq_mulMap_comp, finsuppScalarRight_symm_apply_single, coe_finsuppScalarRight'
finsuppScalarRight' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_finsuppScalarRight' 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarRight	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass
finsuppLeft'_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring zero addCommMonoid leftModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLeft	—	RingHomInvPair.ids Finsupp.smulCommClass IsScalarTower.to_smulCommClass
finsuppLeft_apply 📖	mathematical	—	DFunLike.coe Finsupp TensorProduct zero Finsupp.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring addCommMonoid leftModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLeft LinearMap instModule LinearMap.instFunLike LinearMap.rTensor Finsupp.lapply	—	induction_on RingHomInvPair.ids Finsupp.smulCommClass IsScalarTower.to_smulCommClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.semilinearMapClass finsuppLeft_apply_tmul_apply map_add SemilinearMapClass.toAddHomClass
finsuppLeft_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring zero addCommMonoid leftModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLeft tmul Finsupp.sum Finsupp.single	—	Finsupp.induction_linear RingHomInvPair.ids Finsupp.smulCommClass IsScalarTower.to_smulCommClass zero_tmul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass add_tmul map_add SemilinearMapClass.toAddHomClass Finsupp.sum_add_index Finsupp.single_zero Finsupp.single_add finsuppLEquivDirectSum_single directSumLeft_tmul_lof finsuppLEquivDirectSum_symm_lof Finsupp.sum_single_index
finsuppLeft_apply_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp TensorProduct zero Finsupp.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring addCommMonoid leftModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLeft tmul	—	RingHomInvPair.ids Finsupp.smulCommClass IsScalarTower.to_smulCommClass finsuppLeft_apply_tmul Finsupp.sum_apply Finsupp.sum_eq_single Finsupp.single_eq_of_ne' zero_tmul Finsupp.single_zero Finsupp.single_eq_same
finsuppLeft_smul' 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring zero addCommMonoid leftModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppLeft leftHasSMul Finsupp.distribMulAction SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass addZeroClass addMonoid leftDistribMulAction	—	induction_on RingHomInvPair.ids Finsupp.smulCommClass IsScalarTower.to_smulCommClass smul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.ext finsuppLeft_apply_tmul_apply smul_add map_add SemilinearMapClass.toAddHomClass
finsuppLeft_symm_apply_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp TensorProduct zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring addCommMonoid leftModule IsScalarTower.to_smulCommClass Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppLeft Finsupp.single tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass Finsupp.smulCommClass finsuppLEquivDirectSum_single directSumLeft_symm_lof_tmul finsuppLEquivDirectSum_symm_lof
finsuppRight_apply 📖	mathematical	—	DFunLike.coe Finsupp TensorProduct zero Finsupp.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppRight LinearMap instModule LinearMap.instFunLike LinearMap.lTensor Finsupp.lapply	—	induction_on RingHomInvPair.ids IsScalarTower.to_smulCommClass map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearMap.semilinearMapClass finsuppRight_apply_tmul_apply map_add SemilinearMapClass.toAddHomClass
finsuppRight_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring zero addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppRight tmul Finsupp.sum Finsupp.single	—	Finsupp.induction_linear RingHomInvPair.ids IsScalarTower.to_smulCommClass tmul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass tmul_add map_add SemilinearMapClass.toAddHomClass Finsupp.sum_add_index Finsupp.single_zero Finsupp.single_add finsuppLEquivDirectSum_single directSumRight_tmul_lof Finsupp.sum_single_index finsuppLEquivDirectSum_symm_lof
finsuppRight_apply_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp TensorProduct zero Finsupp.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppRight tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass finsuppRight_apply_tmul Finsupp.sum_apply Finsupp.sum_eq_single Finsupp.single_eq_of_ne' tmul_zero Finsupp.single_zero Finsupp.single_eq_same
finsuppRight_symm_apply_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp TensorProduct zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppRight Finsupp.single tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass finsuppRight_tmul_single
finsuppRight_tmul_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring zero addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppRight tmul Finsupp.single	—	Finsupp.ext RingHomInvPair.ids IsScalarTower.to_smulCommClass finsuppRight_apply_tmul_apply Finsupp.single_apply tmul_zero
finsuppScalarLeft_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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarLeft lid LinearMap LinearMap.instFunLike LinearMap.rTensor Finsupp.lapply	—	RingHomInvPair.ids finsuppLeft_apply
finsuppScalarLeft_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarLeft tmul Finsupp.sum Finsupp.single SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finsupp.ext RingHomInvPair.ids finsuppScalarLeft_apply_tmul_apply Finsupp.sum_apply Finsupp.sum_eq_single Finsupp.single_eq_of_ne' zero_smul Finsupp.single_zero Finsupp.single_eq_same
finsuppScalarLeft_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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarLeft tmul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids finsuppLeft_apply_tmul_apply
finsuppScalarLeft_symm_apply_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule addCommMonoid instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppScalarLeft Finsupp.single tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids LinearEquiv.trans.congr_simp Finsupp.mapRange.linearEquiv_symm Finsupp.mapRange_single LinearEquiv.map_zero finsuppLeft_symm_apply_single
finsuppScalarRight_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarRight AlgebraTensorModule.rid LinearMap instModule LinearMap.instFunLike LinearMap.lTensor Finsupp.lapply	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass finsuppRight_apply
finsuppScalarRight_apply_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarRight tmul Finsupp.sum Finsupp.single SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finsupp.ext RingHomInvPair.ids IsScalarTower.to_smulCommClass finsuppScalarRight_apply_tmul_apply Finsupp.sum_apply Finsupp.sum_eq_single Finsupp.single_eq_of_ne' zero_smul Finsupp.single_zero Finsupp.single_eq_same
finsuppScalarRight_apply_tmul_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarRight tmul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass finsuppRight_apply_tmul_apply
finsuppScalarRight_smul 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppScalarRight leftHasSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SMulZeroClass.toSMul Finsupp.instZero Finsupp.smulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
finsuppScalarRight_symm_apply_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule addCommMonoid leftModule IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppScalarRight Finsupp.single tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass LinearEquiv.trans.congr_simp Finsupp.mapRange.linearEquiv_symm Finsupp.mapRange_single LinearEquiv.map_zero finsuppRight_symm_apply_single

(root)

Definitions

Name	Category	Theorems
finsuppTensorFinsupp 📖	CompOp	3 math math: finsuppTensorFinsupp_apply, finsuppTensorFinsupp_single, finsuppTensorFinsupp_symm_single
finsuppTensorFinsupp' 📖	CompOp	11 math math: finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, finsuppTensorFinsupp'_single_tmul_single, finsuppTensorFinsupp'_symm_single_mul, finsuppTensorFinsupp'_apply_apply, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, Rep.leftRegularTensorTrivialIsoFree_inv_hom, Rep.linearization_δ_hom, finsuppTensorFinsuppRid_self, Rep.leftRegularTensorTrivialIsoFree_hom_hom, finsuppTensorFinsuppLid_self, Rep.linearization_μ_hom
finsuppTensorFinsuppLid 📖	CompOp	4 math math: finsuppTensorFinsuppLid_symm_single_smul, finsuppTensorFinsuppLid_apply_apply, finsuppTensorFinsuppLid_single_tmul_single, finsuppTensorFinsuppLid_self
finsuppTensorFinsuppRid 📖	CompOp	4 math math: finsuppTensorFinsuppRid_symm_single_smul, finsuppTensorFinsuppRid_single_tmul_single, finsuppTensorFinsuppRid_apply_apply, finsuppTensorFinsuppRid_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsuppTensorFinsupp'_apply_apply 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids TensorProduct Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsupp' TensorProduct.tmul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	finsuppTensorFinsuppLid_apply_apply
finsuppTensorFinsupp'_single_tmul_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsupp' TensorProduct.tmul Finsupp.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	finsuppTensorFinsuppLid_single_tmul_single
finsuppTensorFinsupp'_symm_single_eq_single_one_tmul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppTensorFinsupp' Finsupp.single TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids one_mul finsuppTensorFinsupp'_symm_single_mul
finsuppTensorFinsupp'_symm_single_eq_tmul_single_one 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppTensorFinsupp' Finsupp.single TensorProduct.tmul AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomInvPair.ids mul_one finsuppTensorFinsupp'_symm_single_mul
finsuppTensorFinsupp'_symm_single_mul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring TensorProduct Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppTensorFinsupp' Finsupp.single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib TensorProduct.tmul	—	finsuppTensorFinsuppLid_symm_single_smul
finsuppTensorFinsuppLid_apply_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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsuppLid TensorProduct.tmul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids finsuppTensorFinsupp_apply
finsuppTensorFinsuppLid_self 📖	mathematical	—	finsuppTensorFinsuppLid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule finsuppTensorFinsupp'	—	RingHomInvPair.ids
finsuppTensorFinsuppLid_single_tmul_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsuppLid TensorProduct.tmul Finsupp.single SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids finsuppTensorFinsupp_single Finsupp.lcongr_single
finsuppTensorFinsuppLid_symm_single_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppTensorFinsuppLid Finsupp.single SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.tmul	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq finsuppTensorFinsuppLid_single_tmul_single
finsuppTensorFinsuppRid_apply_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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsuppRid TensorProduct.tmul SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids finsuppTensorFinsupp_apply
finsuppTensorFinsuppRid_self 📖	mathematical	—	finsuppTensorFinsuppRid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule finsuppTensorFinsupp'	—	RingHomInvPair.ids finsuppTensorFinsupp'.eq_1 finsuppTensorFinsuppLid.eq_1 finsuppTensorFinsuppRid.eq_1 TensorProduct.lid_eq_rid
finsuppTensorFinsuppRid_single_tmul_single 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsuppRid TensorProduct.tmul Finsupp.single SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	RingHomInvPair.ids finsuppTensorFinsupp_single Finsupp.lcongr_single
finsuppTensorFinsuppRid_symm_single_smul 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid TensorProduct MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Finsupp.module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppTensorFinsuppRid Finsupp.single SMulZeroClass.toSMul DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction TensorProduct.tmul	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq finsuppTensorFinsuppRid_single_tmul_single
finsuppTensorFinsupp_apply 📖	mathematical	—	DFunLike.coe Finsupp TensorProduct TensorProduct.zero Finsupp.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsupp TensorProduct.tmul	—	Finsupp.induction_linear RingHomInvPair.ids Finsupp.smulCommClass IsScalarTower.to_smulCommClass TensorProduct.zero_tmul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass TensorProduct.add_tmul map_add SemilinearMapClass.toAddHomClass TensorProduct.tmul_zero TensorProduct.tmul_add finsuppTensorFinsupp_single Finsupp.single_apply ite_and
finsuppTensorFinsupp_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids TensorProduct Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring TensorProduct.zero TensorProduct.addCommMonoid TensorProduct.leftModule Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.to_smulCommClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv finsuppTensorFinsupp TensorProduct.tmul Finsupp.single	—	RingHomInvPair.ids Finsupp.smulCommClass IsScalarTower.to_smulCommClass finsuppLEquivDirectSum_single TensorProduct.directSum_lof_tmul_lof finsuppLEquivDirectSum_symm_lof
finsuppTensorFinsupp_symm_single 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp TensorProduct TensorProduct.zero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp.instAddCommMonoid Finsupp.module CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.leftModule IsScalarTower.to_smulCommClass Finsupp.smulCommClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm finsuppTensorFinsupp Finsupp.single TensorProduct.tmul	—	RingHomInvPair.ids IsScalarTower.to_smulCommClass Finsupp.smulCommClass LinearEquiv.symm_apply_eq finsuppTensorFinsupp_single

---

← Back to Index