Option

📁 Source: Mathlib/Algebra/BigOperators/Option.lean

Statistics

Metric	Count
Definitions	0
Theorems add_sum_eq_sum_insertNone, mul_prod_eq_prod_insertNone, prod_eraseNone, prod_insertNone, sum_eraseNone, sum_insertNone	6
Total	6

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_sum_eq_sum_insertNone 📖	mathematical	—	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid sum DFunLike.coe OrderEmbedding Finset Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderEmbedding insertNone	—	sum_insertNone
mul_prod_eq_prod_insertNone 📖	mathematical	—	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid prod DFunLike.coe OrderEmbedding Finset Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderEmbedding insertNone	—	prod_insertNone
prod_eraseNone 📖	mathematical	—	prod DFunLike.coe OrderHom Finset PartialOrder.toPreorder partialOrder OrderHom.instFunLike eraseNone Option.elim' MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_map map_some_eraseNone prod_erase
prod_insertNone 📖	mathematical	—	prod DFunLike.coe OrderEmbedding Finset Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderEmbedding insertNone MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	prod_cons prod_map prod_congr
sum_eraseNone 📖	mathematical	—	sum DFunLike.coe OrderHom Finset PartialOrder.toPreorder partialOrder OrderHom.instFunLike eraseNone Option.elim' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_map map_some_eraseNone sum_erase
sum_insertNone 📖	mathematical	—	sum DFunLike.coe OrderEmbedding Finset Preorder.toLE PartialOrder.toPreorder partialOrder instFunLikeOrderEmbedding insertNone AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	sum_cons sum_map sum_congr

---

← Back to Index