NatAntidiagonal

Statistics

Metric	Count
Definitions	0
Theorems `antidiagonal_succ`, `antidiagonal_succ'`, `antidiagonal_succ_succ'`, `antidiagonal_zero`, `card_antidiagonal`, `map_swap_antidiagonal`, `mem_antidiagonal`, `nodup_antidiagonal`	8
Total	8

Name	Kind	Assumes	Proves	Validates	Depends On
`antidiagonal_succ` 📖	mathematical	—	`antidiagonal` `Multiset.cons` `Multiset.map`	—	`List.Nat.antidiagonal_succ`
`antidiagonal_succ'` 📖	mathematical	—	`antidiagonal` `Multiset.cons` `Multiset.map`	—	`antidiagonal.eq_1` `List.Nat.antidiagonal_succ'` `Multiset.coe_add` `Multiset.add_comm` `Multiset.map_coe` `Multiset.cons_coe`
`antidiagonal_succ_succ'` 📖	mathematical	—	`antidiagonal` `Multiset.cons` `Multiset.map`	—	`antidiagonal_succ` `antidiagonal_succ'` `Multiset.map_cons` `Multiset.map_map`
`antidiagonal_zero` 📖	mathematical	—	`antidiagonal` `Multiset` `Multiset.instSingleton`	—	—
`card_antidiagonal` 📖	mathematical	—	`Multiset.card` `antidiagonal`	—	`antidiagonal.eq_1` `Multiset.coe_card` `List.Nat.length_antidiagonal`
`map_swap_antidiagonal` 📖	mathematical	—	`Multiset.map` `antidiagonal`	—	`antidiagonal.eq_1` `Multiset.map_coe` `List.Nat.map_swap_antidiagonal` `Multiset.coe_reverse`
`mem_antidiagonal` 📖	mathematical	—	`Multiset` `Multiset.instMembership` `antidiagonal`	—	`antidiagonal.eq_1` `Multiset.mem_coe` `List.Nat.mem_antidiagonal`
`nodup_antidiagonal` 📖	mathematical	—	`Multiset.Nodup` `antidiagonal`	—	`Multiset.coe_nodup` `List.Nat.nodup_antidiagonal`

---