Commit 2025-05-02 14:44 8a454c28

View on Github →

chore(NumberTheory/Cyclotomic/CyclotomicCharacter): fix name to camelCase (#24521) Fix the name of ModularCyclotomicCharacter and CyclotomicCharacter to camelCase, since they are not Type. Also fix the module docstring.

Estimated changes

Modified Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

deleted theorem CyclotomicCharacter.continuous

deleted theorem CyclotomicCharacter.spec

deleted theorem CyclotomicCharacter.toFun_apply

deleted theorem CyclotomicCharacter.toFun_spec

deleted theorem CyclotomicCharacter.toZModPow

deleted theorem CyclotomicCharacter.toZModPow_toFun

deleted theorem IsPrimitiveRoot.autToPow_eq_ModularCyclotomicCharacter

added theorem IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter

deleted theorem ModularCyclotomicCharacter'.spec'

deleted theorem ModularCyclotomicCharacter'.unique'

deleted def ModularCyclotomicCharacter'

deleted theorem ModularCyclotomicCharacter.aux_spec

deleted theorem ModularCyclotomicCharacter.comp

deleted theorem ModularCyclotomicCharacter.id

deleted theorem ModularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow

deleted theorem ModularCyclotomicCharacter.spec

deleted theorem ModularCyclotomicCharacter.toFun_spec''

deleted theorem ModularCyclotomicCharacter.toFun_spec'

deleted theorem ModularCyclotomicCharacter.toFun_spec

deleted theorem ModularCyclotomicCharacter.toFun_unique'

deleted theorem ModularCyclotomicCharacter.toFun_unique

deleted theorem ModularCyclotomicCharacter.unique

added theorem cyclotomicCharacter.continuous

added theorem cyclotomicCharacter.spec

added theorem cyclotomicCharacter.toFun_apply

added theorem cyclotomicCharacter.toFun_spec

added theorem cyclotomicCharacter.toZModPow

added theorem cyclotomicCharacter.toZModPow_toFun

added theorem modularCyclotomicCharacter'.spec'

added theorem modularCyclotomicCharacter'.unique'

added def modularCyclotomicCharacter'

added theorem modularCyclotomicCharacter.aux_spec

added theorem modularCyclotomicCharacter.comp

added theorem modularCyclotomicCharacter.id

added theorem modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow

added theorem modularCyclotomicCharacter.spec

added theorem modularCyclotomicCharacter.toFun_spec''

added theorem modularCyclotomicCharacter.toFun_spec'

added theorem modularCyclotomicCharacter.toFun_spec

added theorem modularCyclotomicCharacter.toFun_unique'

added theorem modularCyclotomicCharacter.toFun_unique

added theorem modularCyclotomicCharacter.unique