Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.monic.eq_one_of_map_eq_one

Modification history

2021-10-01 10:38
src/data/polynomial/monic.lean
feat(data/polynomial,field_theory): `(minpoly A x).map f ≠ 1` (#9451) …
Added polynomial.monic.eq_one_of_map_eq_oneView on Github →