Documentation Verification Report

Pi

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

Statistics

Metric	Count
Definitions `finAntidiagonal`, `aux`, `piAntidiag`	3
Theorems `finsetCongr_piAntidiag_eq_antidiag`, `map_nsmul_piAntidiag`, `map_nsmul_piAntidiag_univ`, `map_sym_eq_piAntidiag`, `mem_finAntidiagonal`, `mem_piAntidiag`, `nsmul_piAntidiag`, `nsmul_piAntidiag_univ`, `pairwiseDisjoint_piAntidiag_map_addRightEmbedding`, `piAntidiag_cons`, `piAntidiag_empty`, `piAntidiag_empty_of_ne_zero`, `piAntidiag_empty_zero`, `piAntidiag_insert`, `piAntidiag_univ_fin_eq_antidiagonalTuple`, `piAntidiag_zero`	16
Total	19

Finset

Definitions

Name	Category	Theorems
`finAntidiagonal` 📖	CompOp	1 math math: `mem_finAntidiagonal`
`piAntidiag` 📖	CompOp	17 math math: `map_nsmul_piAntidiag_univ`, `sum_pow_eq_sum_piAntidiag`, `piAntidiag_zero`, `map_nsmul_piAntidiag`, `piAntidiag_insert`, `piAntidiag_univ_fin_eq_antidiagonalTuple`, `map_sym_eq_piAntidiag`, `piAntidiag_empty`, `mem_piAntidiag`, `sum_pow_eq_sum_piAntidiag_of_commute`, `piAntidiag_cons`, `pairwiseDisjoint_piAntidiag_map_addRightEmbedding`, `piAntidiag_empty_zero`, `finsetCongr_piAntidiag_eq_antidiag`, `piAntidiag_empty_of_ne_zero`, `nsmul_piAntidiag_univ`, `nsmul_piAntidiag`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsetCongr_piAntidiag_eq_antidiag` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.finsetCongr` `Equiv.boolArrowEquivProd` `piAntidiag` `univ` `Bool.fintype` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid`	—	`ext` `Equiv.injective` `sum_congr` `sum_insert` `sum_singleton` `add_comm`
`map_nsmul_piAntidiag` 📖	mathematical	—	`map` `AddMonoid.toNatSMul` `Pi.addMonoid` `Nat.instAddMonoid` `mul_right_injective₀` `MulZeroClass.toZero` `Nat.instMulZeroClass` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal` `filter` `decidableDforallFinset`	—	`mul_right_injective₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `map_eq_image` `nsmul_piAntidiag`
`map_nsmul_piAntidiag_univ` 📖	mathematical	—	`map` `AddMonoid.toNatSMul` `Pi.addMonoid` `Nat.instAddMonoid` `mul_right_injective₀` `MulZeroClass.toZero` `Nat.instMulZeroClass` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal` `univ` `filter` `Fintype.decidableForallFintype`	—	`mul_right_injective₀` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `filter.congr_simp` `map_nsmul_piAntidiag`
`map_sym_eq_piAntidiag` 📖	mathematical	—	`map` `Sym` `Multiset.count` `Multiset` `Multiset.card` `Sym.toMultiset` `Multiset.count_injective` `Sym.coe_injective` `sym` `piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal`	—	`ext` `Multiset.count_injective` `Sym.coe_injective` `sum_congr` `Multiset.sum_count_eq_card` `Multiset.card_sum` `Multiset.card_nsmul` `Multiset.card_singleton` `mul_one` `Multiset.count_sum'` `Multiset.count_nsmul` `Multiset.count_singleton` `mul_ite` `MulZeroClass.mul_zero` `sum_ite_eq`
`mem_finAntidiagonal` 📖	mathematical	—	`Finset` `instMembership` `finAntidiagonal` `sum` `univ` `Fin.fintype`	—	`Subtype.prop`
`mem_piAntidiag` 📖	mathematical	—	`Finset` `instMembership` `piAntidiag` `sum`	—	`piAntidiag.eq_1` `Trunc.ind` `sum_dite_of_true` `Fintype.sum_equiv` `Subtype.coe_eta` `sum_attach` `Fintype.card_coe`
`nsmul_piAntidiag` 📖	mathematical	—	`Finset` `smulFinset` `AddMonoid.toNatSMul` `Pi.addMonoid` `Nat.instAddMonoid` `piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal` `filter` `decidableDforallFinset`	—	`ext` `mem_smul_finset` `sum_congr` `IsDomain.to_noZeroDivisors` `Nat.instIsDomain` `not_imp_comm` `dvd_zero` `mul_div_cancel_left₀` `Nat.instMulDivCancelClass`
`nsmul_piAntidiag_univ` 📖	mathematical	—	`Finset` `smulFinset` `Fintype.decidablePiFintype` `AddMonoid.toNatSMul` `Pi.addMonoid` `Nat.instAddMonoid` `piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal` `univ` `filter` `Fintype.decidableForallFintype`	—	`filter.congr_simp` `nsmul_piAntidiag`
`pairwiseDisjoint_piAntidiag_map_addRightEmbedding` 📖	mathematical	`Finset` `instMembership`	`Set.PairwiseDisjoint` `partialOrder` `instOrderBot` `SetLike.coe` `instSetLike` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid` `AddCancelCommMonoid.toAddCommMonoid` `map` `addRightEmbedding` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `piAntidiag`	—	`Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `antidiagonal_congr'` `addRightEmbedding.congr_simp` `sum_congr` `sum_add_distrib` `sum_ite_eq'` `add_zero`
`piAntidiag_cons` 📖	mathematical	`Finset` `instMembership`	`piAntidiag` `AddCancelCommMonoid.toAddCommMonoid` `cons` `disjiUnion` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid` `map` `addRightEmbedding` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `pairwiseDisjoint_piAntidiag_map_addRightEmbedding`	—	`ext` `Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `pairwiseDisjoint_piAntidiag_map_addRightEmbedding` `sum_cons` `addRightEmbedding.congr_simp` `sum_update_of_notMem` `Function.update_of_ne` `add_zero` `Function.update_self` `zero_add` `sum_congr` `sum_add_distrib` `sum_ite_eq'`
`piAntidiag_empty` 📖	mathematical	—	`piAntidiag` `Finset` `instEmptyCollection` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSingleton` `Pi.instZero`	—	`piAntidiag_empty_zero` `piAntidiag_empty_of_ne_zero`
`piAntidiag_empty_of_ne_zero` 📖	mathematical	—	`piAntidiag` `Finset` `instEmptyCollection`	—	`eq_empty_of_forall_notMem`
`piAntidiag_empty_zero` 📖	mathematical	—	`piAntidiag` `Finset` `instEmptyCollection` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `instSingleton` `Pi.instZero`	—	`ext`
`piAntidiag_insert` 📖	mathematical	`Finset` `instMembership`	`piAntidiag` `AddCancelCommMonoid.toAddCommMonoid` `instInsert` `biUnion` `HasAntidiagonal.antidiagonal` `AddCommMonoid.toAddMonoid` `image` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`Pi.instIsRightCancelAdd` `AddRightCancelSemigroup.toIsRightCancelAdd` `pairwiseDisjoint_piAntidiag_map_addRightEmbedding` `cons_eq_insert` `add_left_injective` `map_eq_image` `disjiUnion.congr_simp` `disjiUnion_eq_biUnion` `piAntidiag_cons`
`piAntidiag_univ_fin_eq_antidiagonalTuple` 📖	mathematical	—	`piAntidiag` `Nat.instAddCommMonoid` `Nat.instHasAntidiagonal` `univ` `Fin.fintype` `Nat.antidiagonalTuple`	—	`ext`
`piAntidiag_zero` 📖	mathematical	—	`piAntidiag` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Finset` `instSingleton` `Pi.instZero`	—	`ext` `Unique.instSubsingleton`

Finset.finAntidiagonal

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	—

---

← Back to Index