Theorem Set.toFinset_offDiag

Modification history

2026-01-13 17:24
Mathlib/Data/Fintype/Prod.lean
feat: define `List.offDiag` (#33812) …
Added Set.toFinset_offDiagView on Github →