mathlib
31263840 - refactor(data/finset/noncomm_prod): Use `set.pairwise` (#16859)

Commit
3 years ago
refactor(data/finset/noncomm_prod): Use `set.pairwise` (#16859) Redefine the various `noncomm_prod`s 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.
Author
Parents
Loading