Documentation Verification Report

FinsuppEquiv

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

Statistics

Metric	Count
Definitions `finsuppAntidiagEquiv`, `finsuppAntidiagEquivSubtype`	2
Theorems `card_finsuppAntidiag_nat_eq_choose`, `card_finsuppAntidiag_nat_eq_multichoose`, `count_coe_finsuppAntidiagEquiv_apply`, `finsuppAntidiagEquivSubtype_apply_coe`, `finsuppAntidiagEquivSubtype_symm_apply_coe`, `finsuppAntidiagEquiv_symm_apply_apply`	6
Total	8

Finset

Definitions

Name	Category	Theorems
`finsuppAntidiagEquiv` 📖	CompOp	2 math math: `count_coe_finsuppAntidiagEquiv_apply`, `finsuppAntidiagEquiv_symm_apply_apply`
`finsuppAntidiagEquivSubtype` 📖	CompOp	2 math math: `finsuppAntidiagEquivSubtype_apply_coe`, `finsuppAntidiagEquivSubtype_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_finsuppAntidiag_nat_eq_choose` 📖	mathematical	—	`card` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `finsuppAntidiag` `Nat.instHasAntidiagonal` `Nat.choose`	—	`card_eq_of_equiv_fintype` `Sym.card_sym_eq_choose` `Fintype.card_coe`
`card_finsuppAntidiag_nat_eq_multichoose` 📖	mathematical	—	`card` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `finsuppAntidiag` `Nat.instHasAntidiagonal` `Nat.multichoose`	—	`card_eq_of_equiv_fintype` `Sym.card_sym_eq_multichoose` `Fintype.card_coe`
`count_coe_finsuppAntidiagEquiv_apply` 📖	mathematical	—	`Multiset.count` `Finset` `SetLike.instMembership` `instSetLike` `Sym.toMultiset` `DFunLike.coe` `Equiv` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `finsuppAntidiag` `Nat.instHasAntidiagonal` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `finsuppAntidiagEquiv` `Finsupp.instFunLike`	—	`Finsupp.count_toMultiset`
`finsuppAntidiagEquivSubtype_apply_coe` 📖	mathematical	—	`Finsupp` `Finset` `SetLike.instMembership` `instSetLike` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finsupp.sum` `DFunLike.coe` `Equiv` `finsuppAntidiag` `EquivLike.toFunLike` `Equiv.instEquivLike` `finsuppAntidiagEquivSubtype` `Finsupp.subtypeDomain`	—	—
`finsuppAntidiagEquivSubtype_symm_apply_coe` 📖	mathematical	—	`Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `SetLike.instMembership` `instSetLike` `finsuppAntidiag` `DFunLike.coe` `Equiv` `Finsupp.sum` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finsuppAntidiagEquivSubtype` `Finsupp.extendDomain` `decidableMem`	—	—
`finsuppAntidiagEquiv_symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `Finsupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Nat.instAddCommMonoid` `Finsupp.instFunLike` `Finset` `SetLike.instMembership` `instSetLike` `finsuppAntidiag` `Nat.instHasAntidiagonal` `Equiv` `Sym` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finsuppAntidiagEquiv` `Multiset.count` `Sym.toMultiset`	—	`Subtype.coe_eta`

---

← Back to Index