mathlib
2d47c1d6 - feat(ring_theory/polynomial/cyclotomic/*): ɸₙ(1) = 1 (#10483)

Commit
4 years ago
feat(ring_theory/polynomial/cyclotomic/*): ɸₙ(1) = 1 (#10483) (for `n` not a prime power) Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading