Commit 2025-04-08 20:01 2d569030

View on Github →

feat: generalize Mathlib.Data (#23146) This is one of a series of PRs that generalizes type classes across Mathlib. These are generated using a new linter that tries to re-elaborate theorem definitions with more general type classes to see if it succeeds. It will accept the generalization if deleting the entire type class causes the theorem to fail to compile, and the old type class can not simply be re-synthesized with the new declaration. Otherwise, the generalization is rejected as the type class is not being generalized, but can simply be replaced by implicit type class synthesis or an implicit type class in a variable block being pulled in. The linter currently output debug statements indicating source file positions where type classes should be generalized, and a script then makes those edits. This file contains a subset of those generalizations. The linter and the script performing re-writes is available in commit 5e2b7040be0f73821c1dcb360ffecd61235d87af. Also see discussions on Zulip here:

Estimated changes

modified theorem Set.IsPWO.smul
modified theorem Set.IsWF.min_smul
modified theorem Set.IsWF.smul
modified theorem Holor.cprankMax_1
modified theorem Holor.cprankMax_add
modified theorem Holor.cprankMax_mul
modified theorem Holor.cprankMax_nil
modified theorem Holor.cprankMax_sum
modified theorem Holor.cprankMax_upper_bound
modified theorem Holor.mul_scalar_mul
modified theorem Holor.slice_unitVec_mul
modified theorem Holor.sum_unitVec_mul_slice
modified theorem Int.cast_ite
modified theorem Matrix.blockDiagonal_smul
modified theorem Matrix.mulVec_smul
modified theorem Matrix.vecMul_smul
modified theorem NeZero.nat_of_neZero
modified theorem ext_nat''
modified theorem Nat.cast_four
modified theorem Nat.cast_three
modified theorem Nat.cast_two
modified theorem RingHom.ext_zmod
modified theorem ZMod.ringHom_map_cast
modified theorem ZMod.ringHom_rightInverse
modified theorem ZMod.ringHom_surjective