Commit 2023-05-22 18:33 b079bbf3

View on Github →

feat: port FieldTheory.Minpoly.Basic (#4216)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Minpoly/Basic.lean

added theorem minpoly.aeval

added theorem minpoly.aeval_ne_zero_of_dvdNotUnit_minpoly

added theorem minpoly.degree_pos

added theorem minpoly.eq_X_sub_C_of_algebraMap_inj

added theorem minpoly.eq_zero

added theorem minpoly.irreducible

added theorem minpoly.map_ne_one

added theorem minpoly.mem_range_of_degree_eq_one

added theorem minpoly.min

added theorem minpoly.minpoly_algEquiv

added theorem minpoly.minpoly_algHom

added theorem minpoly.monic

added theorem minpoly.natDegree_pos

added theorem minpoly.ne_one

added theorem minpoly.ne_zero

added theorem minpoly.not_isUnit

added theorem minpoly.subsingleton

added theorem minpoly.unique'