Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cyclotomic_eq_minpoly

Modification history

2021-09-09 07:32
src/ring_theory/polynomial/cyclotomic.lean
chore(ring_theory/polynomial/cyclotomic): golf+remove `nontrivial` (#9090)
Deleted cyclotomic_eq_minpolyView on Github →
2021-01-18 23:02
src/ring_theory/polynomial/cyclotomic.lean
refactor(field_theory|ring_theory|linear_algebra): minpoly A x (#5774) …
Added cyclotomic_eq_minpolyView on Github →