Documentation Verification Report

NatAntidiagonal

📁 Source: Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

Statistics

Metric	Count
Definitions `antidiagonalTuple`, `sigmaAntidiagonalTupleEquivTuple`, `antidiagonalTuple`, `antidiagonalTuple`	4
Theorems `antidiagonalTuple_one`, `antidiagonalTuple_two`, `antidiagonalTuple_zero_right`, `antidiagonalTuple_zero_succ`, `antidiagonalTuple_zero_zero`, `mem_antidiagonalTuple`, `sigmaAntidiagonalTupleEquivTuple_apply`, `sigmaAntidiagonalTupleEquivTuple_symm_apply_fst`, `sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe`, `antidiagonalTuple_one`, `antidiagonalTuple_pairwise_pi_lex`, `antidiagonalTuple_two`, `antidiagonalTuple_zero_right`, `antidiagonalTuple_zero_succ`, `antidiagonalTuple_zero_zero`, `mem_antidiagonalTuple`, `nodup_antidiagonalTuple`, `antidiagonalTuple_one`, `antidiagonalTuple_two`, `antidiagonalTuple_zero_right`, `antidiagonalTuple_zero_succ`, `antidiagonalTuple_zero_zero`, `mem_antidiagonalTuple`, `nodup_antidiagonalTuple`	24
Total	28

Finset.Nat

Definitions

Name	Category	Theorems
`antidiagonalTuple` 📖	CompOp	10 math math: `sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe`, `antidiagonalTuple_one`, `sigmaAntidiagonalTupleEquivTuple_symm_apply_fst`, `Finset.piAntidiag_univ_fin_eq_antidiagonalTuple`, `antidiagonalTuple_zero_right`, `antidiagonalTuple_two`, `antidiagonalTuple_zero_zero`, `mem_antidiagonalTuple`, `antidiagonalTuple_zero_succ`, `sigmaAntidiagonalTupleEquivTuple_apply`
`sigmaAntidiagonalTupleEquivTuple` 📖	CompOp	3 math math: `sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe`, `sigmaAntidiagonalTupleEquivTuple_symm_apply_fst`, `sigmaAntidiagonalTupleEquivTuple_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antidiagonalTuple_one` 📖	mathematical	—	`antidiagonalTuple` `Finset` `Finset.instSingleton` `Matrix.vecCons` `Matrix.vecEmpty`	—	`Finset.eq_of_veq` `Multiset.Nat.antidiagonalTuple_one`
`antidiagonalTuple_two` 📖	mathematical	—	`antidiagonalTuple` `Finset.map` `Equiv.toEmbedding` `Equiv.symm` `piFinTwoEquiv` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `instHasAntidiagonal`	—	`Finset.eq_of_veq` `Multiset.Nat.antidiagonalTuple_two`
`antidiagonalTuple_zero_right` 📖	mathematical	—	`antidiagonalTuple` `Finset` `Finset.instSingleton` `Pi.instZero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`Finset.eq_of_veq` `Multiset.Nat.antidiagonalTuple_zero_right`
`antidiagonalTuple_zero_succ` 📖	mathematical	—	`antidiagonalTuple` `Finset` `Finset.instEmptyCollection`	—	—
`antidiagonalTuple_zero_zero` 📖	mathematical	—	`antidiagonalTuple` `Finset` `Finset.instSingleton` `Matrix.vecEmpty`	—	—
`mem_antidiagonalTuple` 📖	mathematical	—	`Finset` `Finset.instMembership` `antidiagonalTuple` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Fin.fintype`	—	`List.Nat.mem_antidiagonalTuple`
`sigmaAntidiagonalTupleEquivTuple_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Finset` `SetLike.instMembership` `Finset.instSetLike` `antidiagonalTuple` `EquivLike.toFunLike` `Equiv.instEquivLike` `sigmaAntidiagonalTupleEquivTuple`	—	—
`sigmaAntidiagonalTupleEquivTuple_symm_apply_fst` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `antidiagonalTuple` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sigmaAntidiagonalTupleEquivTuple` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Fin.fintype`	—	—
`sigmaAntidiagonalTupleEquivTuple_symm_apply_snd_coe` 📖	mathematical	—	`Finset` `SetLike.instMembership` `Finset.instSetLike` `antidiagonalTuple` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Fin.fintype` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `sigmaAntidiagonalTupleEquivTuple`	—	—

List.Nat

Definitions

Name	Category	Theorems
`antidiagonalTuple` 📖	CompOp	8 math math: `antidiagonalTuple_two`, `antidiagonalTuple_zero_zero`, `antidiagonalTuple_one`, `antidiagonalTuple_zero_right`, `antidiagonalTuple_zero_succ`, `mem_antidiagonalTuple`, `antidiagonalTuple_pairwise_pi_lex`, `nodup_antidiagonalTuple`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antidiagonalTuple_one` 📖	mathematical	—	`antidiagonalTuple` `Matrix.vecCons` `Matrix.vecEmpty`	—	`add_assoc` `add_tsub_cancel_left` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `antidiagonalTuple_zero_succ`
`antidiagonalTuple_pairwise_pi_lex` 📖	mathematical	—	`Pi.Lex` `antidiagonalTuple`	—	`antidiagonal_zero` `antidiagonal_succ`
`antidiagonalTuple_two` 📖	mathematical	—	`antidiagonalTuple` `Matrix.vecCons` `Matrix.vecEmpty` `antidiagonal`	—	`antidiagonalTuple.eq_3` `antidiagonalTuple_one`
`antidiagonalTuple_zero_right` 📖	mathematical	—	`antidiagonalTuple` `Pi.instZero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`Unique.instSubsingleton` `Fin.isEmpty'` `antidiagonalTuple.eq_3` `antidiagonal_zero` `Matrix.cons_zero_zero`
`antidiagonalTuple_zero_succ` 📖	mathematical	—	`antidiagonalTuple`	—	—
`antidiagonalTuple_zero_zero` 📖	mathematical	—	`antidiagonalTuple` `Matrix.vecEmpty`	—	—
`mem_antidiagonalTuple` 📖	mathematical	—	`antidiagonalTuple` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Fin.fintype`	—	`Finset.sum_congr` `Finset.univ_eq_empty` `Fin.isEmpty'` `Fin.sum_cons`
`nodup_antidiagonalTuple` 📖	mathematical	—	`antidiagonalTuple`	—	`List.Nodup.map` `Fin.cons_right_injective` `antidiagonal_succ` `Function.onFun.eq_1`

Multiset.Nat

Definitions

Name	Category	Theorems
`antidiagonalTuple` 📖	CompOp	7 math math: `antidiagonalTuple_one`, `antidiagonalTuple_zero_right`, `antidiagonalTuple_two`, `mem_antidiagonalTuple`, `nodup_antidiagonalTuple`, `antidiagonalTuple_zero_succ`, `antidiagonalTuple_zero_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antidiagonalTuple_one` 📖	mathematical	—	`antidiagonalTuple` `Multiset` `Multiset.instSingleton` `Matrix.vecCons` `Matrix.vecEmpty`	—	`List.Nat.antidiagonalTuple_one`
`antidiagonalTuple_two` 📖	mathematical	—	`antidiagonalTuple` `Multiset.map` `Matrix.vecCons` `Matrix.vecEmpty` `antidiagonal`	—	`List.Nat.antidiagonalTuple_two`
`antidiagonalTuple_zero_right` 📖	mathematical	—	`antidiagonalTuple` `Multiset` `Multiset.instSingleton` `Pi.instZero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`List.Nat.antidiagonalTuple_zero_right`
`antidiagonalTuple_zero_succ` 📖	mathematical	—	`antidiagonalTuple` `Multiset` `Multiset.instZero`	—	—
`antidiagonalTuple_zero_zero` 📖	mathematical	—	`antidiagonalTuple` `Multiset` `Multiset.instSingleton` `Matrix.vecEmpty`	—	—
`mem_antidiagonalTuple` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `antidiagonalTuple` `Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `Fin.fintype`	—	`List.Nat.mem_antidiagonalTuple`
`nodup_antidiagonalTuple` 📖	mathematical	—	`Multiset.Nodup` `antidiagonalTuple`	—	`List.Nat.nodup_antidiagonalTuple`

---

← Back to Index