mathlib3
36ea9e84 - chore(*): cleanup imports (#3511)

Commit
6 years ago
chore(*): cleanup imports (#3511) A not-very-interesting cleanup of imports. I deleted ``` instance orbit_fintype (b : β) [fintype α] [decidable_eq β] : fintype (orbit α b) := set.fintype_range _ ``` which wasn't being used, for the sake of not having to import everything about finiteness into `algebra.group_action`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading