Documentation Verification Report

PointwiseSMul

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

Statistics

Metric	Count
Definitions `instSMulForallOfIsLeftCancelVAddOfSMulWithZero`, `vaddAntidiagonal`	2
Theorems `finite_vaddAntidiagonal`, `mem_vaddAntidiagonal_iff`, `mem_vaddAntidiagonal_of_addGroup`, `smul_apply_addAction`, `smul_eq`	5
Total	7

Finsupp

Definitions

Name	Category	Theorems
`instSMulForallOfIsLeftCancelVAddOfSMulWithZero` 📖	CompOp	2 math math: `smul_eq`, `smul_apply_addAction`
`vaddAntidiagonal` 📖	CompOp	3 math math: `mem_vaddAntidiagonal_of_addGroup`, `smul_eq`, `mem_vaddAntidiagonal_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_vaddAntidiagonal` 📖	mathematical	—	`Set.Finite` `Set.vaddAntidiagonal` `SetLike.coe` `Finset` `Finset.instSetLike` `support` `Function.support`	—	`Set.Finite.of_injOn` `IsLeftCancelVAdd.left_cancel` `Finset.finite_toSet`
`mem_vaddAntidiagonal_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `vaddAntidiagonal` `HVAdd.hVAdd` `instHVAdd`	—	`finite_vaddAntidiagonal`
`mem_vaddAntidiagonal_of_addGroup` 📖	mathematical	—	`Finset` `Finset.instMembership` `vaddAntidiagonal` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instIsLeftCancelVAdd_1` `HVAdd.hVAdd` `instHVAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`instIsLeftCancelVAdd_1` `mem_vaddAntidiagonal_iff` `eq_neg_vadd_iff`
`smul_apply_addAction` 📖	mathematical	—	`Finsupp` `instSMulForallOfIsLeftCancelVAddOfSMulWithZero` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddAction.toAddSemigroupAction` `instIsLeftCancelVAdd_1` `Finset.sum` `support` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulWithZero.toSMulZeroClass` `DFunLike.coe` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`instIsLeftCancelVAdd_1` `smul_eq` `Finset.sum_of_injOn` `mem_vaddAntidiagonal_of_addGroup` `Finset.mem_coe` `mem_support_iff` `mem_vaddAntidiagonal_iff` `zero_smul` `smul_zero`
`smul_eq` 📖	mathematical	—	`Finsupp` `instSMulForallOfIsLeftCancelVAddOfSMulWithZero` `Finset.sum` `vaddAntidiagonal` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SMulZeroClass.toSMul` `SMulWithZero.toSMulZeroClass` `DFunLike.coe` `instFunLike`	—	—

---

← Back to Index