Commit 2023-05-22 22:00 bdf3e422

View on Github →

feat: port FieldTheory.Minpoly.Field (#4232)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Minpoly/Field.lean

added theorem minpoly.add_algebraMap

added theorem minpoly.aeval_of_isScalarTower

added theorem minpoly.aux_inj_roots_of_min_poly

added theorem minpoly.coeff_zero_eq_zero

added theorem minpoly.coeff_zero_ne_zero

added theorem minpoly.degree_le_of_ne_zero

added theorem minpoly.dvd

added theorem minpoly.dvd_map_of_isScalarTower

added theorem minpoly.dvd_map_of_is_scalar_tower'

added theorem minpoly.eq_X_sub_C'

added theorem minpoly.eq_X_sub_C

added theorem minpoly.eq_of_algebraMap_eq

added theorem minpoly.eq_of_irreducible

added theorem minpoly.eq_of_irreducible_of_monic

added theorem minpoly.ne_zero_of_finite_field_extension

added theorem minpoly.one

added theorem minpoly.prime

added theorem minpoly.root

added theorem minpoly.sub_algebraMap

added theorem minpoly.unique

added theorem minpoly.zero