Documentation Verification Report

SMul

📁 Source: Mathlib/Algebra/Polynomial/Eval/SMul.lean

Statistics

Metric	Count
Definitions `leval`	1
Theorems `eval_smul`, `eval₂_smul`, `leval_apply`, `map_smul`, `smul_comp`	5
Total	6

Polynomial

Definitions

Name	Category	Theorems
`leval` 📖	CompOp	3 math math: `leval_eq_smeval.linearMap`, `leval_apply`, `leval_coe_eq_smeval`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_smul` 📖	mathematical	—	`eval` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`smul_one_smul` `isScalarTower` `eval.eq_1` `eval₂_smul` `RingHom.id_apply` `smul_one_mul` `eval₂_id`
`eval₂_smul` 📖	mathematical	—	`eval₂` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`LE.le.trans_lt` `natDegree_smul_le` `eval₂_eq_sum` `sum_over_range'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `MulZeroClass.zero_mul` `Finset.sum_congr` `coeff_smul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_assoc` `Finset.mul_sum`
`leval_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `leval` `eval`	—	—
`map_smul` 📖	mathematical	—	`map` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	—	`map.eq_1` `eval₂_smul` `RingHom.comp_apply` `C_mul'`
`smul_comp` 📖	mathematical	—	`comp` `Polynomial` `SMulZeroClass.toSMul` `instZero` `smulZeroClass`	—	`smul_one_smul` `isScalarTower` `comp.eq_1` `eval₂_smul` `smul_eq_C_mul` `smul_assoc` `one_smul`

---

← Back to Index