Commit 2025-06-04 10:11 ba688d88

View on Github →

chore(Data): remove primes from names (#25163) This PR renames lemmas that use a ', addressing technical debt. This focuses on declarations that seem simple to rename.

Estimated changes

Modified Mathlib/Data/Finset/Functor.lean

Modified Mathlib/Data/Finset/Lattice/Fold.lean

deleted theorem Finset.sup_singleton''

deleted theorem Finset.sup_singleton'

added theorem Finset.sup_singleton_apply

added theorem Finset.sup_singleton_eq_self

Modified Mathlib/Data/Int/Init.lean

deleted theorem Int.toNat_lt''

added theorem Int.toNat_lt_of_ne_zero

Modified Mathlib/Data/Int/NatPrime.lean

Modified Mathlib/Data/Nat/ChineseRemainder.lean

added theorem Nat.modEq_list_map_prod_iff

deleted theorem Nat.modEq_list_prod_iff'

Modified Mathlib/Data/Nat/Pairing.lean

added theorem Nat.pair_eq_of_unpair_eq

deleted theorem Nat.pair_unpair'

Modified Mathlib/Data/Nat/Prime/Basic.lean

deleted theorem Nat.not_prime_mul'

added theorem Nat.not_prime_of_mul_eq

Modified Mathlib/Logic/Equiv/List.lean

Modified Mathlib/Order/Partition/Finpartition.lean

Modified Mathlib/Tactic/NormNum/Prime.lean

Modified scripts/nolints_prime_decls.txt