Commit 2025-03-19 14:41 d2c823e7

View on Github →

feat: generalize Mathlib.Data.Num.Lemmas (#23060) Note: In addition to generalization, this PR collapses ofZNum_toNat into cast_ofZNum since it is now superfluous by the simpNF linter. 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 711029291b0d50626b5174b00548fcb4e93f62c5. Also see discussion on Zulip here: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/498862988 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Elab.20to.20generalize.20type.20classes.20for.20theorems/near/501288855

Estimated changes

modified theorem Num.cast_add
modified theorem Num.cast_bit0
modified theorem Num.cast_bit1
modified theorem Num.cast_inj
modified theorem Num.cast_lt
modified theorem Num.cast_mul
modified theorem Num.cast_ofZNum
modified theorem Num.cast_toZNumNeg
modified theorem PosNum.cast_lt
modified theorem PosNum.cast_mul
modified theorem PosNum.cast_pos
modified theorem PosNum.one_le_cast
modified theorem ZNum.cast_inj
modified theorem ZNum.cast_lt
modified theorem ZNum.cast_mul
modified theorem ZNum.cast_sub
modified theorem ZNum.cast_zneg