SMul

📁 Source: Mathlib/Data/Finsupp/SMul.lean

Statistics

Metric	Count
Definitions single, comapDistribMulAction, comapMulAction, comapSMul, distribMulAction	5
Theorems comapDomain_smul, comapDomain_smul_of_injective, comapSMul_apply, comapSMul_def, comapSMul_single, distribMulActionHom_ext, distribMulActionHom_ext', distribMulActionHom_ext'_iff, faithfulSMul, filter_smul, mapDomain_smul, moduleIsTorsionFree, single_smul, smul_single', smul_single_one, sum_smul_index, sum_smul_index', sum_smul_index_addMonoidHom, support_smul_eq, finsupp	20
Total	25

Finsupp

Definitions

Name	Category	Theorems
comapDistribMulAction 📖	CompOp	—
comapMulAction 📖	CompOp	—
comapSMul 📖	CompOp	3 math math: comapSMul_single, comapSMul_def, comapSMul_apply
distribMulAction 📖	CompOp	2 math math: TensorProduct.finsuppLeft_smul', distribMulActionHom_ext'_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comapDomain_smul 📖	mathematical	Set.InjOn Set.preimage SetLike.coe Finset Finset.instSetLike support Finsupp SMulZeroClass.toSMul instZero smulZeroClass Set.InjOn.mono Set.preimage_mono Set Set.instHasSubset Finset.instHasSubset Finset.coe_subset support_smul	comapDomain	—	ext
comapDomain_smul_of_injective 📖	mathematical	—	comapDomain Finsupp SMulZeroClass.toSMul instZero smulZeroClass Function.Injective.injOn Set.preimage SetLike.coe Finset Finset.instSetLike support	—	comapDomain_smul Function.Injective.injOn
comapSMul_apply 📖	mathematical	—	DFunLike.coe Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike comapSMul DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smul_inv_smul mapDomain_apply MulAction.injective
comapSMul_def 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid comapSMul mapDomain SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	—
comapSMul_single 📖	mathematical	—	Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid comapSMul single SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	mapDomain_single
distribMulActionHom_ext 📖	—	DFunLike.coe DistribMulActionHom MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid distribMulAction DistribMulActionHom.instFunLike single	—	—	DistribMulActionHom.toAddMonoidHom_injective addHom_ext DistribMulActionSemiHomClass.toAddMonoidHomClass DistribMulActionHom.instDistribMulActionSemiHomClassCoeMonoidHom
distribMulActionHom_ext' 📖	—	DistribMulActionHom.comp MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid distribMulAction DistribMulActionHom.single MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId	—	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId distribMulActionHom_ext DistribMulActionHom.congr_fun
distribMulActionHom_ext'_iff 📖	mathematical	—	DistribMulActionHom.comp MonoidHom.id MulOneClass.toMulOne Monoid.toMulOneClass Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid distribMulAction DistribMulActionHom.single MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId	—	MonoidHom.CompTriple.instId_comp MonoidHom.CompTriple.instIsId distribMulActionHom_ext'
faithfulSMul 📖	mathematical	—	FaithfulSMul Finsupp SMulZeroClass.toSMul instZero smulZeroClass	—	FaithfulSMul.eq_of_smul_eq_smul smul_single single_eq_same DFunLike.congr_fun
filter_smul 📖	mathematical	—	filter Finsupp SMulZeroClass.toSMul instZero smulZeroClass	—	DFunLike.coe_injective filter_eq_indicator Set.indicator_const_smul
mapDomain_smul 📖	mathematical	—	mapDomain Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass	—	mapDomain_mapRange smul_zero smul_add
moduleIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid module	—	ext IsRegular.isSMulRegular
single_smul 📖	mathematical	—	SMulZeroClass.toSMul SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulActionWithZero.toSMulWithZero DFunLike.coe Finsupp instFunLike single	—	single_eq_same single_eq_of_ne' zero_smul
smul_single' 📖	mathematical	—	Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instDistribSMul single Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	smul_single
smul_single_one 📖	mathematical	—	Finsupp MulZeroClass.toZero MulZeroOneClass.toMulZeroClass SMulZeroClass.toSMul instZero smulZeroClass SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero single MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	smul_single smul_eq_mul mul_one
sum_smul_index 📖	mathematical	MulZeroClass.toZero AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum Finsupp SMulZeroClass.toSMul instZero smulZeroClass SMulWithZero.toSMulZeroClass MulZeroClass.toSMulWithZero MulZeroClass.toMul	—	sum_mapRange_index smul_zero
sum_smul_index' 📖	mathematical	AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	sum Finsupp SMulZeroClass.toSMul instZero smulZeroClass	—	sum_mapRange_index smul_zero
sum_smul_index_addMonoidHom 📖	mathematical	—	sum AddZero.toZero AddZeroClass.toAddZero Finsupp SMulZeroClass.toSMul instZero smulZeroClass DFunLike.coe AddMonoidHom AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidHom.instFunLike	—	sum_mapRange_index smul_zero AddMonoidHom.map_zero
support_smul_eq 📖	mathematical	—	support AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Finsupp SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finset.ext IsDomain.toIsCancelMulZero

Finsupp.DistribMulActionHom

Definitions

Name	Category	Theorems
single 📖	CompOp	1 math math: Finsupp.distribMulActionHom_ext'_iff

IsSMulRegular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finsupp 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul	Finsupp Finsupp.instZero Finsupp.smulZeroClass	—	Finsupp.ext DFunLike.congr_fun

---

← Back to Index