Commit 2024-12-20 05:03 bee1d789

View on Github →

chore: rename ZMod.IsUnit_cast_of_dvd (#19997)

Estimated changes

Modified Mathlib/Data/ZMod/Units.lean

deleted theorem ZMod.IsUnit_cast_of_dvd

added theorem ZMod.isUnit_cast_of_dvd

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean