Commit 2023-04-02 23:34 00fcb9a9

View on Github →

chore: fix casing in RingTheory.Polynomial.Basic (#3218)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/Basic.lean

added def Ideal.degreeLE

deleted def Ideal.degreeLe

added theorem Ideal.is_fg_degreeLE

deleted theorem Ideal.is_fg_degreeLe

added def Polynomial.degreeLE

added theorem Polynomial.degreeLE_eq_span_X_pow

added theorem Polynomial.degreeLE_mono

added def Polynomial.degreeLT

added def Polynomial.degreeLTEquiv

added theorem Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero

added theorem Polynomial.degreeLT_eq_span_X_pow

added theorem Polynomial.degreeLT_mono

deleted def Polynomial.degreeLe

deleted theorem Polynomial.degreeLe_eq_span_X_pow

deleted theorem Polynomial.degreeLe_mono

deleted def Polynomial.degreeLt

deleted def Polynomial.degreeLtEquiv

deleted theorem Polynomial.degreeLtEquiv_eq_zero_iff_eq_zero

deleted theorem Polynomial.degreeLt_eq_span_X_pow

deleted theorem Polynomial.degreeLt_mono

added theorem Polynomial.eval_eq_sum_degreeLTEquiv

deleted theorem Polynomial.eval_eq_sum_degreeLtEquiv

added theorem Polynomial.mem_degreeLE

added theorem Polynomial.mem_degreeLT

deleted theorem Polynomial.mem_degreeLe

deleted theorem Polynomial.mem_degreeLt