cyclotomic): `is_root_cyclotomic_iff` (#10422)

Commit

4 years ago

feat(ring_theory/polynomial/cyclotomic): `is_root_cyclotomic_iff` (#10422) From the flt-regular project. Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>

Author

ericrbg

Parents

6f745cd2

mathlib 8915dc8e - feat(ring_theory/polynomial/cyclotomic): `is_root_cyclotomic_iff` (#10422)

mathlib
8915dc8e - feat(ring_theory/polynomial/cyclotomic): `is_root_cyclotomic_iff` (#10422)