Commit 2023-08-24 16:07 a57b2c25

View on Github →

feat: Data.Finset.NatAntidiagonal.antidiagonal_equiv_fin (#6766) as suggested by @ocfnash in https://github.com/leanprover-community/mathlib4/pull/6425#discussion_r1304089614

Estimated changes

Modified Mathlib/Data/Finset/NatAntidiagonal.lean

added theorem Finset.Nat.antidiagonal.fst_lt

added theorem Finset.Nat.antidiagonal.snd_lt

added def Finset.Nat.antidiagonal_equiv_fin

added theorem Finset.Nat.antidiagonal_subtype_ext