Documentation Verification Report

NatAntidiagonal

📁 Source: Mathlib/Data/Finset/NatAntidiagonal.lean

Statistics

Metric	Count
Definitions `antidiagonalEquivFin`, `instHasAntidiagonal`	2
Theorems `fst_lt`, `snd_lt`, `antidiagonalEquivFin_apply_val`, `antidiagonalEquivFin_symm_apply_coe`, `antidiagonal_eq_image`, `antidiagonal_eq_image'`, `antidiagonal_eq_map`, `antidiagonal_eq_map'`, `antidiagonal_filter_fst_le_of_le`, `antidiagonal_filter_le_fst_of_le`, `antidiagonal_filter_le_snd_of_le`, `antidiagonal_filter_snd_le_of_le`, `antidiagonal_succ`, `antidiagonal_succ'`, `antidiagonal_succ_succ'`, `antidiagonal_zero`, `card_antidiagonal`	17
Total	19

Finset.Nat

Definitions

Name	Category	Theorems
`antidiagonalEquivFin` 📖	CompOp	2 math math: `antidiagonalEquivFin_symm_apply_coe`, `antidiagonalEquivFin_apply_val`
`instHasAntidiagonal` 📖	CompOp	75 math math: `Finset.map_nsmul_piAntidiag_univ`, `Finset.sum_pow_eq_sum_piAntidiag`, `LieDerivation.iterate_apply_lie`, `sum_antidiagonal_eq_sum_range_succ`, `antidiagonal_eq_image'`, `sum_antidiagonal_subst`, `prod_antidiagonal_succ`, `Finset.sum_antidiagonal_choose_succ_mul`, `prod_antidiagonal_swap`, `Tree.treesOfNumNodesEq_succ`, `antidiagonal_succ_succ'`, `antidiagonal_eq_image`, `antidiagonalEquivFin_symm_apply_coe`, `Ring.add_choose_eq`, `Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag`, `MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero`, `Finset.map_nsmul_piAntidiag`, `antidiagonal_eq_map`, `antidiagonal_succ`, `DividedPowers.OfInvertibleFactorial.dpow_add`, `Finset.piAntidiag_univ_fin_eq_antidiagonalTuple`, `Finset.map_sym_eq_piAntidiag`, `sum_antidiagonal_eq_sum_range_succ_mk`, `PowerSeries.coeff_inv_aux`, `prod_antidiagonal_eq_prod_range_succ`, `Finset.sum_antidiagonal_choose_succ_nsmul`, `Finsupp.antidiagonal_single`, `PowerSeries.coeff_invOfUnit`, `antidiagonalTuple_two`, `card_antidiagonal`, `antidiagonal_zero`, `DividedPowers.dpow_add`, `bernoulli_spec'`, `Polynomial.coeff_mul`, `LieAlgebra.ad_pow_lie`, `prod_antidiagonal_succ'`, `Ring.descPochhammer_smeval_add`, `Nat.bell_succ'`, `bernoulli'_spec'`, `Polynomial.hasseDeriv_mul`, `PolynomialModule.smul_apply`, `sum_antidiagonal_swap`, `MvPolynomial.mul_esymm_eq_sum`, `Finset.sum_antidiagonal_choose_add`, `Finset.prod_antidiagonal_pow_choose_succ`, `prod_antidiagonal_eq_prod_range_succ_mk`, `PowerSeries.coeff_mul`, `prod_antidiagonal_subst`, `Finset.sum_pow_eq_sum_piAntidiag_of_commute`, `Commute.add_pow'`, `LieModule.toEnd_pow_lie`, `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'`, `PowerSeries.coeff_prod`, `DividedPowers.OfInvertibleFactorial.dpow_add_of_lt`, `PowerSeries.coeff_inv`, `PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2`, `Nat.fib_succ_eq_sum_choose`, `antidiagonal_filter_le_fst_of_le`, `MvPolynomial.psum_eq_mul_esymm_sub_sum`, `antidiagonal_filter_snd_le_of_le`, `summable_sum_mul_antidiagonal_of_summable_norm'`, `catalan_succ'`, `antidiagonal_eq_map'`, `summable_norm_sum_mul_antidiagonal_of_summable_norm`, `antidiagonal_filter_fst_le_of_le`, `antidiagonal_filter_le_snd_of_le`, `PowerSeries.coeff_pow`, `sum_antidiagonal_succ`, `Nat.add_choose_eq`, `antidiagonalEquivFin_apply_val`, `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm`, `antidiagonal_succ'`, `Finset.nsmul_piAntidiag_univ`, `sum_antidiagonal_succ'`, `Finset.nsmul_piAntidiag`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antidiagonalEquivFin_apply_val` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `EquivLike.toFunLike` `Equiv.instEquivLike` `antidiagonalEquivFin`	—	—
`antidiagonalEquivFin_symm_apply_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `antidiagonalEquivFin`	—	—
`antidiagonal_eq_image` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.image` `Finset.range`	—	`Finset.map_eq_image`
`antidiagonal_eq_image'` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.image` `Finset.range`	—	`antidiagonal_eq_map'` `Finset.map_eq_image`
`antidiagonal_eq_map` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.map` `Finset.range`	—	—
`antidiagonal_eq_map'` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.map` `Finset.range`	—	`Prod.swap_injective` `Finset.map_swap_antidiagonal` `antidiagonal_eq_map` `Finset.map_map`
`antidiagonal_filter_fst_le_of_le` 📖	mathematical	—	`Finset.filter` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.map` `Function.Embedding.prodMap` `Function.Embedding.refl` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid`	—	`add_comm` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.map_prodComm_antidiagonal` `Finset.filter.congr_simp` `antidiagonal_filter_snd_le_of_le` `Finset.map_map` `Finset.ext`
`antidiagonal_filter_le_fst_of_le` 📖	mathematical	—	`Finset.filter` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.map` `Function.Embedding.prodMap` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Function.Embedding.refl`	—	`Finset.ext` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `add_right_comm`
`antidiagonal_filter_le_snd_of_le` 📖	mathematical	—	`Finset.filter` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.map` `Function.Embedding.prodMap` `Function.Embedding.refl` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid`	—	`add_comm` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.map_prodComm_antidiagonal` `Finset.filter.congr_simp` `antidiagonal_filter_le_fst_of_le` `Finset.map_map` `Finset.ext`
`antidiagonal_filter_snd_le_of_le` 📖	mathematical	—	`Finset.filter` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.map` `Function.Embedding.prodMap` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddCancelCommMonoid.toAddCancelMonoid` `Nat.instAddCancelCommMonoid` `Function.Embedding.refl`	—	`Finset.ext` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `add_comm` `tsub_add_eq_add_tsub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `add_assoc` `add_tsub_cancel_right`
`antidiagonal_succ` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.cons` `Finset.map` `Function.Embedding.prodMap` `Nat.succ_injective` `Function.Embedding.refl`	—	`Finset.eq_of_veq` `Nat.succ_injective` `Finset.cons_val` `Finset.map_val` `Multiset.Nat.antidiagonal_succ`
`antidiagonal_succ'` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.cons` `Finset.map` `Function.Embedding.prodMap` `Function.Embedding.refl` `Nat.succ_injective`	—	`Finset.eq_of_veq` `Nat.succ_injective` `Finset.cons_val` `Finset.map_val` `Multiset.Nat.antidiagonal_succ'`
`antidiagonal_succ_succ'` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset.cons` `Finset.map` `Function.Embedding.prodMap` `Nat.succ_injective`	—	`Nat.succ_injective` `antidiagonal_succ` `antidiagonal_succ'` `Finset.cons.congr_simp` `Finset.map_cons` `Finset.map_map`
`antidiagonal_zero` 📖	mathematical	—	`Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal` `Finset` `Finset.instSingleton`	—	—
`card_antidiagonal` 📖	mathematical	—	`Finset.card` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal`	—	`Multiset.Nat.card_antidiagonal`

Finset.Nat.antidiagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_lt` 📖	—	`Finset` `Finset.instMembership` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal`	—	—	`Finset.antidiagonal.fst_le` `Nat.instCanonicallyOrderedAdd`
`snd_lt` 📖	—	`Finset` `Finset.instMembership` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal`	—	—	`Finset.antidiagonal.snd_le` `Nat.instCanonicallyOrderedAdd`

---

← Back to Index