Commit 2026-10-27 12:01 c6257e96

View on Github →

chore: rename coe_int lemmas to intCast (#44826) This renames Lean 3 style coe_int in lemma names about Int.cast to intCast. 🤖 Generated with Claude Code

Estimated changes

Modified Mathlib/Data/Rat/Defs.lean

deleted theorem Rat.coe_int_num_of_den_eq_one

added theorem Rat.intCast_num_of_den_eq_one

Modified Mathlib/Data/ZMod/Units.lean

deleted theorem ZMod.coe_int_inv_mul_eq_one

deleted theorem ZMod.coe_int_isUnit_iff_isCoprime

deleted theorem ZMod.coe_int_mul_inv_eq_one

deleted theorem ZMod.coe_int_mul_val_inv

deleted theorem ZMod.coe_int_val_inv_mul

added theorem ZMod.intCast_inv_mul_eq_one

added theorem ZMod.intCast_mul_inv_eq_one

added theorem ZMod.intCast_mul_val_inv

added theorem ZMod.intCast_val_inv_mul

added theorem ZMod.isUnit_intCast_iff_isCoprime

Modified Mathlib/NumberTheory/Bernoulli.lean

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean

deleted theorem LiouvilleWith.ne_cast_int

added theorem LiouvilleWith.ne_intCast

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

deleted theorem IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int

added theorem IsPrimitiveRoot.zmodEquivZPowers_apply_intCast