mathlib3

5c5d818d - chore(data/fintype/basic): make units.fintype computable (#9846)

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