Commit 2022-10-13 08:46 1a170053

View on Github →

feat(data/set/finite): Add off_diag finitary instance and lemmas (#16923) Adds a fintype instance for off_diag, finite lemmas for it, and adds a related missing prod lemma.

Estimated changes

Modified src/data/fintype/basic.lean

added theorem set.to_finset_off_diag

Modified src/data/set/finite.lean

added theorem set.finite.off_diag

added theorem set.finite.to_finset_off_diag

added theorem set.finite.to_finset_prod