Commit 2023-12-22 22:10 503aade4

View on Github →

feat: Antidiagonal lemmas (#9224) From LeanAPAP

Estimated changes

Modified Mathlib/Data/Finset/Antidiagonal.lean

added theorem Finset.antidiagonal_congr'

modified theorem Finset.antidiagonal_congr

modified theorem Finset.antidiagonal_subtype_ext

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

added theorem Finset.Nat.antidiagonal_eq_image'

added theorem Finset.Nat.antidiagonal_eq_image

added theorem Finset.Nat.antidiagonal_eq_map'

added theorem Finset.Nat.antidiagonal_eq_map