Documentation Verification Report

Finsupp

📁 Source: Mathlib/Algebra/Order/Antidiag/Finsupp.lean

Statistics

Metric	Count
Definitions `finsuppAntidiag`	1
Theorems `finsuppAntidiag_empty`, `finsuppAntidiag_empty_of_ne_zero`, `finsuppAntidiag_empty_zero`, `finsuppAntidiag_insert`, `finsuppAntidiag_mono`, `finsuppAntidiag_zero`, `mapRange_finsuppAntidiag_eq`, `mapRange_finsuppAntidiag_subset`, `mem_finsuppAntidiag`, `mem_finsuppAntidiag'`, `mem_finsuppAntidiag_insert`	11
Total	12

Finset

Definitions

Name	Category	Theorems
`finsuppAntidiag` 📖	CompOp	16 math math: `MvPowerSeries.coeff_pow`, `mem_finsuppAntidiag`, `Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag`, `mem_finsuppAntidiag_insert`, `finsuppAntidiag_empty_of_ne_zero`, `mapRange_finsuppAntidiag_eq`, `mapRange_finsuppAntidiag_subset`, `MvPowerSeries.coeff_prod`, `finsuppAntidiag_mono`, `PowerSeries.coeff_prod`, `finsuppAntidiag_empty_zero`, `finsuppAntidiag_empty`, `finsuppAntidiag_insert`, `finsuppAntidiag_zero`, `mem_finsuppAntidiag'`, `PowerSeries.coeff_pow`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsuppAntidiag_empty` 📖	mathematical	—	`finsuppAntidiag` `Finset` `instEmptyCollection` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSingleton` `Finsupp.instZero`	—	`finsuppAntidiag_empty_zero` `finsuppAntidiag_empty_of_ne_zero`
`finsuppAntidiag_empty_of_ne_zero` 📖	mathematical	—	`finsuppAntidiag` `Finset` `instEmptyCollection` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`eq_empty_of_forall_notMem`
`finsuppAntidiag_empty_zero` 📖	mathematical	—	`finsuppAntidiag` `Finset` `instEmptyCollection` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp` `instSingleton` `Finsupp.instZero`	—	`ext` `filter.congr_simp` `filter_empty` `DFunLike.coe_fn_eq` `piAntidiag_empty_zero`
`finsuppAntidiag_insert` 📖	mathematical	`Finset` `instMembership`	`finsuppAntidiag` `instInsert` `biUnion` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.instDecidableEq` `HasAntidiagonal.antidiagonal` `map` `Finsupp.update` `attach`	—	`ext` `mem_finsuppAntidiag_insert` `mem_biUnion`
`finsuppAntidiag_mono` 📖	mathematical	`Finset` `instHasSubset`	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `finsuppAntidiag`	—	`HasSubset.Subset.trans` `instIsTransSubset`
`finsuppAntidiag_zero` 📖	mathematical	—	`finsuppAntidiag` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp` `Finset` `instSingleton` `Finsupp.instZero`	—	`ext` `filter.congr_simp` `DFunLike.coe_fn_eq` `piAntidiag_zero`
`mapRange_finsuppAntidiag_eq` 📖	mathematical	—	`map` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Equiv.toEmbedding` `AddEquiv.toEquiv` `Finsupp.instAdd` `Finsupp.mapRange.addEquiv` `finsuppAntidiag` `DFunLike.coe` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike`	—	`ext` `mapRange_finsuppAntidiag_subset` `AddEquiv.eq_symm_apply` `mem_map_equiv` `map_map` `Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding` `map_refl`
`mapRange_finsuppAntidiag_subset` 📖	mathematical	—	`Finset` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instHasSubset` `map` `Equiv.toEmbedding` `AddEquiv.toEquiv` `Finsupp.instAdd` `Finsupp.mapRange.addEquiv` `finsuppAntidiag` `DFunLike.coe` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike`	—	`AddEquiv.map_zero` `Finsupp.sum_mapRange_index` `map_finsuppSum` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `subset_trans` `instIsTransSubset` `Finsupp.support_mapRange`
`mem_finsuppAntidiag` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instMembership` `finsuppAntidiag` `sum` `DFunLike.coe` `Finsupp.instFunLike` `instHasSubset` `Finsupp.support`	—	—
`mem_finsuppAntidiag'` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instMembership` `finsuppAntidiag` `Finsupp.sum` `instHasSubset` `Finsupp.support`	—	`Finsupp.sum_of_support_subset`
`mem_finsuppAntidiag_insert` 📖	mathematical	`Finset` `instMembership`	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `finsuppAntidiag` `instInsert` `HasAntidiagonal.antidiagonal` `Finsupp.update`	—	`sum_insert` `Finsupp.update_erase_eq_update` `Finsupp.update_self` `sum_congr` `Finsupp.erase_ne` `Finsupp.support_erase` `subset_insert_iff` `Finsupp.coe_update` `Function.update_self` `Function.update_of_ne` `HasSubset.Subset.trans` `instIsTransSubset` `Finsupp.support_update_subset` `insert_subset_insert`

---

← Back to Index