Documentation Verification Report

ToFinsupp

📁 Source: Mathlib/Data/List/ToFinsupp.lean

Statistics

Metric	Count
Definitions `toFinsupp`	1
Theorems `coe_toFinsupp`, `toFinsupp_append`, `toFinsupp_apply`, `toFinsupp_apply_fin`, `toFinsupp_apply_le`, `toFinsupp_apply_lt`, `toFinsupp_concat_eq_toFinsupp_add_single`, `toFinsupp_cons_eq_single_add_embDomain`, `toFinsupp_eq_sum_mapIdx_single`, `toFinsupp_nil`, `toFinsupp_singleton`, `toFinsupp_support`	12
Total	13

List

Definitions

Name	Category	Theorems
`toFinsupp` 📖	CompOp	12 math math: `toFinsupp_eq_sum_mapIdx_single`, `toFinsupp_support`, `toFinsupp_cons_eq_single_add_embDomain`, `toFinsupp_apply_fin`, `coe_toFinsupp`, `toFinsupp_concat_eq_toFinsupp_add_single`, `toFinsupp_apply_le`, `toFinsupp_singleton`, `toFinsupp_apply_lt`, `toFinsupp_apply`, `toFinsupp_append`, `toFinsupp_nil`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_toFinsupp` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `toFinsupp`	—	—
`toFinsupp_append` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `Finsupp.instAdd` `Finsupp.embDomain` `addLeftEmbedding` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `AddLeftCancelMonoid.toAddLeftCancelSemigroup` `AddCancelCommMonoid.toAddLeftCancelMonoid` `Nat.instAddCancelCommMonoid`	—	`Finsupp.ext` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `lt_or_ge` `getD_append` `Finsupp.embDomain_notin_range` `add_zero` `getD_append_right` `getD_eq_default` `zero_add` `Finsupp.embDomain_apply_self`
`toFinsupp_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `toFinsupp`	—	—
`toFinsupp_apply_fin` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `toFinsupp`	—	`getD_eq_getElem`
`toFinsupp_apply_le` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `toFinsupp`	—	`getD_eq_default`
`toFinsupp_apply_lt` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `Finsupp.instFunLike` `toFinsupp`	—	`getD_eq_getElem`
`toFinsupp_concat_eq_toFinsupp_add_single` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `Finsupp.instAdd` `Finsupp.single`	—	`AddLeftCancelSemigroup.toIsLeftCancelAdd` `toFinsupp_append` `toFinsupp_singleton` `Finsupp.embDomain_single` `addLeftEmbedding_apply` `add_zero`
`toFinsupp_cons_eq_single_add_embDomain` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `Finsupp` `Finsupp.instAdd` `Finsupp.single` `Finsupp.embDomain` `Nat.succ_injective`	—	`Nat.succ_injective` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Lean.Meta.FastSubsingleton.elim` `Lean.Meta.instFastSubsingletonForall` `Lean.Meta.instFastSubsingletonDecidable` `toFinsupp_singleton` `Function.Embedding.ext` `add_comm` `toFinsupp_append`
`toFinsupp_eq_sum_mapIdx_single` 📖	mathematical	—	`toFinsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `Finsupp` `Finsupp.instAdd` `Finsupp.instZero` `Finsupp.single`	—	`toFinsupp_nil` `toFinsupp_concat_eq_toFinsupp_add_single` `AddSemigroup.to_isLawfulIdentity` `AddSemigroup.to_isAssociative` `add_zero`
`toFinsupp_nil` 📖	mathematical	—	`toFinsupp` `Finsupp` `Finsupp.instZero`	—	`Finsupp.ext`
`toFinsupp_singleton` 📖	mathematical	—	`toFinsupp` `Finsupp.single`	—	`Finsupp.ext` `zero_add` `Finsupp.single_eq_same` `Finsupp.single_eq_of_ne`
`toFinsupp_support` 📖	mathematical	—	`Finsupp.support` `toFinsupp` `Finset.filter` `Finset.range`	—	—

---

← Back to Index