Commit 2026-01-13 17:24 ad934715

View on Github →

feat: define List.offDiag (#33812) Use it to drop decidability assumption in Finset.offDiag. Also redefine Finset.diag.

Estimated changes

modified theorem Finset.prod_diag
modified theorem Set.Finite.toFinset_offDiag
modified def Finset.diag
modified theorem Finset.diag_insert
modified theorem Finset.diag_inter
modified theorem Finset.diag_mono
modified theorem Finset.diag_singleton
modified theorem Finset.diag_union
modified theorem Finset.diag_union_offDiag
modified def Finset.offDiag
modified theorem Finset.offDiag_card
modified theorem Finset.offDiag_insert
modified theorem Finset.offDiag_inter
modified theorem Finset.offDiag_singleton
modified theorem Finset.offDiag_union
modified theorem Finset.product_sdiff_diag
modified theorem Finset.sym2_eq_image
added theorem Set.toFinset_offDiag
deleted theorem Set.toFinset_off_diag
added theorem List.Nodup.mem_offDiag
added theorem List.length_offDiag'
added theorem List.length_offDiag
added theorem List.nodup_offDiag
added def List.offDiag
added theorem List.offDiag_cons_perm
added theorem List.offDiag_nil
added theorem List.offDiag_singleton
modified theorem Finset.coe_infsep
modified theorem Set.Finset.coe_einfsep
modified theorem Set.einfsep_of_fintype
modified theorem Set.infsep_of_fintype