Commit 2022-08-16 16:11 2ccfe543

View on Github →

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.

Estimated changes

Modified src/algebra/big_operators/fin.lean

Modified src/algebra/big_operators/norm_num.lean

added theorem tactic.norm_num.finset.mk_congr

Modified src/analysis/normed_space/multilinear.lean

Modified src/data/finset/fin.lean

deleted theorem finset.coe_fin_range

deleted def finset.fin_range

deleted theorem finset.fin_range_card

deleted theorem finset.mem_fin_range

Modified src/data/finset/sort.lean

Modified src/data/fintype/basic.lean

modified theorem fin.univ_def

Modified src/data/list/range.lean

Modified test/norm_num_ext.lean