Commit 2023-12-17 19:25 1515c7e8

View on Github →

feat: Dual basis of power basis wrt trace form (#8835)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero'

added theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero

Created Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

added theorem coeff_minpolyDiv

added theorem coeff_minpolyDiv_mem_adjoin

added theorem coeff_minpolyDiv_sub_pow_mem_span

added theorem eval_minpolyDiv_of_aeval_eq_zero

added theorem eval_minpolyDiv_self

added theorem eval₂_minpolyDiv_of_eval₂_eq_zero

added theorem eval₂_minpolyDiv_self

added theorem minpolyDiv_eq_of_isIntegrallyClosed

added theorem minpolyDiv_eq_zero

added theorem minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero

added theorem minpolyDiv_monic

added theorem minpolyDiv_ne_zero

added theorem minpolyDiv_spec

added theorem natDegree_minpolyDiv

added theorem natDegree_minpolyDiv_lt

added theorem natDegree_minpolyDiv_succ

added theorem span_coeff_minpolyDiv

added theorem sum_smul_minpolyDiv_eq_X_pow

Modified Mathlib/FieldTheory/Separable.lean

added theorem Polynomial.Separable.aeval_derivative_ne_zero

added theorem Polynomial.Separable.eval₂_derivative_ne_zero

Modified Mathlib/RingTheory/IntegralClosure.lean

added theorem Submodule.span_range_natDegree_eq_adjoin

Modified Mathlib/RingTheory/Trace.lean

added theorem traceForm_dualBasis_powerBasis_eq