mathlib3

1a170053 - feat(data/set/finite): Add `off_diag` finitary instance and lemmas (#16923)

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. Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>