mathlib3
2ccfe543 - refactor(data/finset/fin): Delete `finset.fin_range` (#15538)

Commit
3 years ago
refactor(data/finset/fin): Delete `finset.fin_range` (#15538) `finset.fin_range n` is just `finset.univ`, so we inline its definition in the `fintype (fin n)` instance to avoid people trying to use it. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Author
Parents
Loading