Commit 2020-07-08 14:31 27f622ef

View on Github →

chore(data/fintype/basic): split, and reduce imports (#3319) Following on from #3256 and #3235, this slices a little out of data.fintype.basic, and reduces imports, mostly in the vicinity of data.fintype.basic.

Estimated changes

Modified src/combinatorics/composition.lean

Modified src/control/bifunctor.lean

Modified src/control/bitraversable/basic.lean

Modified src/control/bitraversable/instances.lean

Modified src/data/equiv/list.lean

Modified src/data/finset/basic.lean

added def finset.fin_range

added theorem finset.fin_range_card

added theorem finset.mem_fin_range

Modified src/data/finset/sort.lean

added theorem finset.mono_of_fin_unique'

Modified src/data/fintype/basic.lean

deleted theorem finset.mono_of_fin_unique'

Created src/data/fintype/sort.lean

Modified src/data/polynomial.lean

Modified src/data/set/basic.lean

Modified src/data/set/intervals/basic.lean

Modified src/group_theory/perm/sign.lean

Modified src/linear_algebra/multilinear.lean

Modified src/order/rel_classes.lean

Modified src/tactic/equiv_rw.lean