Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-24 08:22 5fd3186f

View on Github →

lint(/finsupp/): use finite instead of fintype (#17553) Also golf some proofs.

Estimated changes

Modified src/data/finsupp/defs.lean

added def finsupp.equiv_fun_on_finite

added theorem finsupp.equiv_fun_on_finite_single

added theorem finsupp.equiv_fun_on_finite_symm_coe

added theorem finsupp.equiv_fun_on_finite_symm_single

deleted def finsupp.equiv_fun_on_fintype

deleted theorem finsupp.equiv_fun_on_fintype_single

deleted theorem finsupp.equiv_fun_on_fintype_symm_coe

deleted theorem finsupp.equiv_fun_on_fintype_symm_single

Modified src/data/finsupp/fin.lean

Modified src/data/finsupp/fintype.lean

Modified src/data/finsupp/pwo.lean

modified theorem finsupp.is_pwo

Modified src/data/finsupp/well_founded.lean

Modified src/field_theory/finite/polynomial.lean

Modified src/linear_algebra/basic.lean

added theorem finsupp.linear_equiv_fun_on_finite_single

added theorem finsupp.linear_equiv_fun_on_finite_symm_coe

added theorem finsupp.linear_equiv_fun_on_finite_symm_single

deleted theorem finsupp.linear_equiv_fun_on_fintype_single

deleted theorem finsupp.linear_equiv_fun_on_fintype_symm_coe

deleted theorem finsupp.linear_equiv_fun_on_fintype_symm_single

Modified src/linear_algebra/basis.lean

Modified src/linear_algebra/dimension.lean

Modified src/linear_algebra/dual.lean

Modified src/linear_algebra/finite_dimensional.lean

Modified src/linear_algebra/finsupp.lean

Modified src/linear_algebra/invariant_basis_number.lean

Modified src/set_theory/cardinal/basic.lean