Theorem unique'

Modification history

2025-02-14 11:25
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
chore(NumberTheory/Cyclotomic): remove unique' from root namespace (#21868) …
Deleted unique'View on Github →
2024-03-18 09:20
Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
feat: add mod n cyclotomic character (#6342) …
Added unique'View on Github →