Commit 2023-01-11 06:42 91a95124

View on Github →

feat: Port/data.list.nat antidiagonal (#1474)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/NatAntidiagonal.lean

added def List.Nat.antidiagonal

added theorem List.Nat.antidiagonal_succ'

added theorem List.Nat.antidiagonal_succ

added theorem List.Nat.antidiagonal_succ_succ'

added theorem List.Nat.antidiagonal_zero

added theorem List.Nat.length_antidiagonal

added theorem List.Nat.map_swap_antidiagonal

added theorem List.Nat.mem_antidiagonal

added theorem List.Nat.nodup_antidiagonal