Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-06 03:47 5cba21d8

View on Github →

chore(*): swap order of [fintype A] [decidable_eq A] (#3705) @fpvandoorn suggested in #3603 swapping the order of some [fintype A] [decidable_eq A] arguments to solve a linter problem with slow typeclass lookup. The reasoning is that Lean solves typeclass search problems from right to left, and

  • it's "less likely" that a type is a fintype than it has decidable_eq, so we can fail earlier if fintype comes second
  • typeclass search for [decidable_eq] can already be slow, so it's better to avoid it. This PR applies this suggestion across the library.

Estimated changes

modified def encodable.fintype_pi
modified theorem finset.card_univ_diff
modified def fintype.equiv_fin
modified def fintype.of_surjective
modified def quotient.fin_choice
modified theorem quotient.fin_choice_eq
modified theorem finset.prod_fiberwise
modified theorem fintype.card_fun
modified theorem fintype.card_pi
modified theorem fintype.prod_fiberwise
modified def matrix.scalar