Documentation Verification Report

SMulWithZero

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

Statistics

Metric	Count
Definitions `distribSMul`, `instSMulWithZero`, `smulZeroClass`, `SMulWithZero`	4
Theorems `coe_smul`, `isCentralScalar`, `isScalarTower`, `mapRange_smul`, `mapRange_smul'`, `smulCommClass`, `smul_apply`, `smul_single`, `support_smul`	9
Total	13

Finsupp

Definitions

Name	Category	Theorems
`distribSMul` 📖	CompOp	—
`instSMulWithZero` 📖	CompOp	—
`smulZeroClass` 📖	CompOp	61 math math: `instSMulPosReflectLE`, `IsSMulRegular.finsupp`, `instPosSMulReflectLE`, `floorDiv_def`, `SkewMonoidAlgebra.ofFinsupp_smul`, `filter_smul`, `SkewMonoidAlgebra.toFinsupp_smul`, `sum_smul_index'`, `coe_ceilDiv_def`, `sum_smul_index_linearMap'`, `smulCommClass`, `comapDomain_smul_of_injective`, `Algebra.TensorProduct.basis_repr_tmul`, `sum_smul_index`, `TensorProduct.finsuppLeft_smul'`, `Algebra.TensorProduct.basisAux_map_smul`, `DFinsupp.toFinsupp_smul`, `floorDiv_apply`, `mapRange_smul`, `Module.Basis.isScalarTower_finsupp`, `ceilDiv_apply`, `instFaithfulSMulOfNonempty`, `ceilDiv_def`, `LinearMap.CompatibleSMul.finsupp_dom`, `TensorProduct.finsuppScalarRight_smul`, `instSMulPosReflectLT`, `Nat.ceilRoot_def`, `support_ceilDiv_subset`, `instSMulPosMono`, `Algebra.TensorProduct.basisAux_tmul`, `sigmaFinsuppEquivDFinsupp_smul`, `instPosSMulStrictMono`, `smul_single'`, `Nat.factorization_ceilRoot`, `smul_apply`, `LinearMap.CompatibleSMul.finsupp_cod`, `groupHomology.inhomogeneousChains.d_single`, `isCentralScalar`, `MultilinearMap.freeFinsuppEquiv_apply`, `mapRange_smul'`, `coe_smul`, `support_floorDiv_subset`, `toDFinsupp_smul`, `MultilinearMap.freeFinsuppEquiv_single`, `support_smul`, `instPosSMulMono`, `KaehlerDifferential.kerTotal_mkQ_single_smul`, `Nat.factorization_floorRoot`, `coe_floorDiv`, `Nat.floorRoot_def`, `instSMulPosStrictMono`, `sum_smul_index_semilinearMap'`, `support_smul_eq`, `sum_smul_index_addMonoidHom`, `faithfulSMul`, `smul_single_one`, `smul_single`, `Module.Presentation.tautologicalRelations_relation`, `isScalarTower`, `mapDomain_smul`, `exteriorPower.presentation.relations_relation`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `Function.hasSMul`	—	—
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `MulOpposite`	—	`ext` `IsCentralScalar.op_smul_eq_smul`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	`ext` `smul_assoc`
`mapRange_smul` 📖	mathematical	`SMulZeroClass.toSMul`	`mapRange` `Finsupp` `instZero` `smulZeroClass`	—	`mapRange_smul'`
`mapRange_smul'` 📖	mathematical	`SMulZeroClass.toSMul`	`mapRange` `Finsupp` `instZero` `smulZeroClass`	—	`ext`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	`ext` `SMulCommClass.smul_comm`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `instFunLike` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	—
`smul_single` 📖	mathematical	—	`Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `single`	—	`mapRange_single` `smul_zero`
`support_smul` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `Finsupp` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	`smul_zero`

(root)

Definitions

Name	Category	Theorems
`SMulWithZero` 📖	CompData	—

---

← Back to Index