Commit 2024-01-25 15:54 c27bc4e1

View on Github →

refactor(ZMod): remove coe out of ZMod (#9839)

Estimated changes

Modified Mathlib/Data/ZMod/Algebra.lean

Modified Mathlib/Data/ZMod/Basic.lean

modified theorem Prod.fst_zmod_cast

modified theorem Prod.snd_zmod_cast

modified def ZMod.cast

modified theorem ZMod.castHom_apply

modified theorem ZMod.cast_add'

modified theorem ZMod.cast_add

added theorem ZMod.cast_add_eq_ite

modified theorem ZMod.cast_eq_val

modified theorem ZMod.cast_int_cast'

modified theorem ZMod.cast_int_cast

modified theorem ZMod.cast_mul'

modified theorem ZMod.cast_mul

modified theorem ZMod.cast_nat_cast'

modified theorem ZMod.cast_nat_cast

modified theorem ZMod.cast_neg

modified theorem ZMod.cast_neg_one

modified theorem ZMod.cast_one'

modified theorem ZMod.cast_one

modified theorem ZMod.cast_pow'

modified theorem ZMod.cast_pow

modified theorem ZMod.cast_sub'

modified theorem ZMod.cast_sub

modified theorem ZMod.cast_zero

deleted theorem ZMod.coe_add_eq_ite

modified theorem ZMod.coe_int_cast

modified theorem ZMod.int_cast_cast

modified theorem ZMod.int_cast_comp_cast

modified theorem ZMod.int_cast_rightInverse

modified theorem ZMod.int_cast_zmod_cast

modified theorem ZMod.nat_cast_comp_val

modified theorem ZMod.nat_cast_val

modified theorem ZMod.ringHom_map_cast

Modified Mathlib/Data/ZMod/Module.lean

Modified Mathlib/Data/ZMod/Quotient.lean

Modified Mathlib/Data/ZMod/Units.lean

modified theorem ZMod.IsUnit_cast_of_dvd

Modified Mathlib/GroupTheory/Complement.lean

Modified Mathlib/NumberTheory/DirichletCharacter/Basic.lean

Modified Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean

modified theorem ZMod.χ₈'_eq_χ₄_mul_χ₈

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

modified theorem PadicInt.cast_toZModPow

modified theorem PadicInt.toZMod_spec