Documentation Verification Report

Action

📁 Source: Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_smul`, `smul_prod`, `smul_prod'`, `smul_prod_perm`, `smul_sum`, `smul_prod`, `smul_prod'`, `smul_sum`, `vadd_sum`, `smul_prod`, `smul_prod'`, `smul_sum`, `vadd_sum`, `smul_finprod'`, `smul_finprod_perm`, `smul_finsum_mem`	16
Total	16

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_smul` 📖	mathematical	—	`prod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `CommMonoid.toMonoid` `MulAction.toSemigroupAction`	—	`cons_induction_on` `one_smul` `prod_cons` `smul_mul_smul_comm` `IsScalarTower.left`
`smul_prod` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toNatPow` `card` `prod`	—	`Multiset.map_map` `Multiset.map_congr` `Multiset.smul_prod` `Multiset.card_map`
`smul_prod'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `CommMonoid.toMonoid` `prod`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`smul_prod_perm` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `CommMonoid.toMonoid` `prod` `univ`	—	`smul_prod'` `prod_congr` `smul_smul` `prod_bijective` `Group.mulLeft_bijective`
`smul_sum` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `sum`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_prod` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toNatPow` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`pow_zero` `one_smul` `pow_succ'` `smul_mul_smul_comm` `IsScalarTower.left`
`smul_prod'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne`	—	`map_list_prod` `MonoidHom.instMonoidHomClass`
`smul_sum` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	—	`map_list_sum` `AddMonoidHom.instAddMonoidHomClass`
`vadd_sum` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toNatSMul` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`zero_nsmul` `zero_vadd` `succ_nsmul'` `vadd_add_vadd_comm` `VAddAssocClass.left`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_prod` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toNatPow` `card` `prod` `map`	—	`Quot.induction_on` `List.smul_prod`
`smul_prod'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `CommMonoid.toMonoid` `prod` `map`	—	`MonoidHom.map_multiset_prod`
`smul_sum` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `sum` `map`	—	`AddMonoidHom.map_multiset_sum`
`vadd_sum` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `AddAction.toAddSemigroupAction` `AddMonoid.toNatSMul` `card` `sum` `map`	—	`Quot.induction_on` `List.vadd_sum`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_finprod'` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `CommMonoid.toMonoid` `finprod`	—	`nonempty_fintype` `instFinitePLift` `finprod_eq_prod_plift_of_mulSupport_subset` `Finset.coe_univ` `Finset.smul_prod'`
`smul_finprod_perm` 📖	mathematical	—	`SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulDistribMulAction.toMulAction` `CommMonoid.toMonoid` `finprod`	—	`nonempty_fintype` `finprod_eq_prod_of_fintype` `Finset.smul_prod_perm`
`smul_finsum_mem` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `finsum` `Set` `Set.instMembership`	—	`AddMonoidHom.map_finsum_mem`

---

← Back to Index