mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

refactor(data/finset/noncomm_prod): Use `set.pairwise`

Open YaelDillies opened this issue 3 years ago • 0 comments

Redefine the various noncomm_prods using set.pairwise. This has the advantage of having a solid API around monotonicity in the set or in the relation and avoiding checking the trivial i = j case.

Open in Gitpod

YaelDillies avatar Oct 07 '22 20:10 YaelDillies