mathlib3
81ba17f9 - Removed `finsupp.` prefix; removed redundant variable declarations

Commit

4 years ago

Removed `finsupp.` prefix; removed redundant variable declarations `[decidable_eq α]` was causing the linter to fail

References

Author

stuart-presnell

Parents