Mathlib Changelog
v4
Changelog
About
Github
Theorem
rootsOfUnity.integer_power_of_ringEquiv
Modification history
2024-03-18 09:20
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
feat: add mod n cyclotomic character (#6342) …
Added
rootsOfUnity.integer_power_of_ringEquiv
View on Github →