Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-23 17:11 5c5d818d

View on Github →

chore(data/fintype/basic): make units.fintype computable (#9846) This also:

  • renames equiv.units_equiv_ne_zero to units_equiv_ne_zero, and resolves the TODO comment about generalization
  • renames and generalizes finite_field.card_units to fintype.card_units, and proves it right next to the fintype instance
  • generalizes some typeclass assumptions in finite_field.basic as the linter already required me to tweak them

Estimated changes

modified theorem fintype.card_subtype_eq'
modified theorem fintype.card_subtype_eq
added theorem fintype.card_units
deleted theorem finite_field.card_units
modified theorem finite_field.sum_pow_units