Documentation Verification Report

Pointwise

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

Statistics

Metric	Count
Definitions `instMul`, `instMulZeroClass`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocRing`, `instNonUnitalNonAssocSemiring`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instSemigroupWithZero`, `pointwiseModule`, `pointwiseScalar`, `pointwiseScalarSemiring`	12
Theorems `coe_mul`, `coe_pointwise_smul`, `mul_apply`, `single_mul`, `support_mul`, `support_mul_subset_left`, `support_mul_subset_right`	7
Total	19

Finsupp

Definitions

Name	Category	Theorems
`instMul` 📖	CompOp	10 math math: `QuadraticMap.sum_polar_sub_repr_sq`, `support_mul`, `support_mul_subset_right`, `single_mul`, `mul_apply`, `QuadraticMap.apply_linearCombination'`, `QuadraticMap.apply_linearCombination`, `support_mul_subset_left`, `QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar`, `coe_mul`
`instMulZeroClass` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRing` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	—
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instSemigroupWithZero` 📖	CompOp	—
`pointwiseModule` 📖	CompOp	—
`pointwiseScalar` 📖	CompOp	—
`pointwiseScalarSemiring` 📖	CompOp	1 math math: `coe_pointwise_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instFunLike` `instMul` `Pi.instMul` `MulZeroClass.toMul`	—	—
`coe_pointwise_smul` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instFunLike` `pointwiseScalarSemiring` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `Pi.addZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `Pi.nonUnitalNonAssocSemiring`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `instFunLike` `instMul` `MulZeroClass.toMul`	—	—
`single_mul` 📖	mathematical	—	`single` `MulZeroClass.toZero` `MulZeroClass.toMul` `Finsupp` `instMul`	—	`zipWith_single_single`
`support_mul` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `MulZeroClass.toZero` `Finsupp` `instMul` `Finset.instInter`	—	`Finset.subset_inter` `support_mul_subset_left` `support_mul_subset_right`
`support_mul_subset_left` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `MulZeroClass.toZero` `Finsupp` `instMul`	—	`MulZeroClass.zero_mul`
`support_mul_subset_right` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `support` `MulZeroClass.toZero` `Finsupp` `instMul`	—	`MulZeroClass.mul_zero`

---

← Back to Index