Documentation Verification Report

Module

📁 Source: Mathlib/Data/DFinsupp/Module.lean

Statistics

Metric	Count
Definitions `coeFnLinearMap`, `distribMulAction`, `distribMulAction₂`, `filterLinearMap`, `instSMulZeroClass`, `subtypeDomainLinearMap`	6
Theorems `coeFnLinearMap_apply`, `coe_smul`, `comapDomain'_smul`, `comapDomain_smul`, `equivProdDFinsupp_smul`, `filterLinearMap_apply`, `filter_smul`, `isCentralScalar`, `isScalarTower`, `mk_smul`, `single_smul`, `smulCommClass`, `smul_apply`, `subtypeDomainLinearMap_apply`, `subtypeDomain_smul`, `support_smul`	16
Total	22

DFinsupp

Definitions

Name	Category	Theorems
`coeFnLinearMap` 📖	CompOp	6 math math: `Pi.comul_comp_dFinsuppCoeFnLinearMap`, `range_mapRangeLinearMap`, `Pi.counit_comp_dFinsuppCoeFnLinearMap`, `ker_mapRangeLinearMap`, `coeFnLinearMap_apply`, `Pi.comul_coe_dFinsupp`
`distribMulAction` 📖	CompOp	2 math math: `MultilinearMap.dfinsuppFamily_smul`, `MultilinearMap.freeFinsuppEquiv_def`
`distribMulAction₂` 📖	CompOp	—
`filterLinearMap` 📖	CompOp	2 math math: `Submodule.biSup_eq_range_dfinsupp_lsum`, `filterLinearMap_apply`
`instSMulZeroClass` 📖	CompOp	28 math math: `equivProdDFinsupp_smul`, `smul_apply`, `instSMulPosMono`, `smulCommClass`, `toFinsupp_smul`, `mapRange_smul`, `filter_smul`, `MultilinearMap.freeDFinsuppEquiv_single`, `instPosSMulStrictMono`, `sigmaCurry_smul`, `comapDomain_smul`, `sigmaFinsuppEquivDFinsupp_smul`, `coe_smul`, `instPosSMulReflectLE`, `instPosSMulMono`, `isScalarTower`, `sigmaUncurry_smul`, `Finsupp.toDFinsupp_smul`, `instSMulPosReflectLT`, `comapDomain'_smul`, `MultilinearMap.freeDFinsuppEquiv_apply`, `single_smul`, `isCentralScalar`, `instSMulPosReflectLE`, `subtypeDomain_smul`, `mk_smul`, `support_smul`, `instSMulPosStrictMono`
`subtypeDomainLinearMap` 📖	CompOp	1 math math: `subtypeDomainLinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFnLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `Pi.addCommMonoid` `module` `Pi.module` `LinearMap.instFunLike` `coeFnLinearMap` `instDFunLike`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `instDFunLike` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `Pi.instSMul`	—	—
`comapDomain'_smul` 📖	mathematical	—	`comapDomain'` `DFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`ext` `smul_apply` `comapDomain'_apply`
`comapDomain_smul` 📖	mathematical	—	`comapDomain` `DFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`ext` `smul_apply` `comapDomain_apply`
`equivProdDFinsupp_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `DFinsupp` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivProdDFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass` `Prod.instSMul`	—	`smul_apply` `comapDomain_smul` `Option.some_injective`
`filterLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `module` `LinearMap.instFunLike` `filterLinearMap` `filter`	—	—
`filter_smul` 📖	mathematical	—	`filter` `DFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`ext` `smul_ite` `smul_zero`
`isCentralScalar` 📖	mathematical	`IsCentralScalar` `SMulZeroClass.toSMul` `MulOpposite`	`DFinsupp` `instZero` `instSMulZeroClass`	—	`ext` `IsCentralScalar.op_smul_eq_smul`
`isScalarTower` 📖	mathematical	`IsScalarTower` `SMulZeroClass.toSMul`	`DFinsupp` `instZero` `instSMulZeroClass`	—	`ext` `smul_assoc`
`mk_smul` 📖	mathematical	—	`Pi.instSMul` `Set.Elem` `SetLike.coe` `Finset` `Finset.instSetLike` `Set` `Set.instMembership` `SMulZeroClass.toSMul` `DFinsupp` `instZero` `instSMulZeroClass`	—	`ext` `smul_zero`
`single_smul` 📖	mathematical	—	`single` `SMulZeroClass.toSMul` `DFinsupp` `instZero` `instSMulZeroClass`	—	`ext` `single_apply` `smul_zero`
`smulCommClass` 📖	mathematical	`SMulCommClass` `SMulZeroClass.toSMul`	`DFinsupp` `instZero` `instSMulZeroClass`	—	`ext` `SMulCommClass.smul_comm`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `DFinsupp` `instDFunLike` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	—
`subtypeDomainLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `DFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `addCommMonoid` `module` `LinearMap.instFunLike` `subtypeDomainLinearMap` `subtypeDomain`	—	—
`subtypeDomain_smul` 📖	mathematical	—	`subtypeDomain` `DFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`DFunLike.coe_injective`
`support_smul` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `DFinsupp` `SMulZeroClass.toSMul` `instZero` `instSMulZeroClass`	—	`support_mapRange`

---

← Back to Index