Commit 2023-03-23 13:00 d033c086

View on Github →

feat: port Data.Polynomial.DenomsClearable (#2978)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/DenomsClearable.lean

added theorem DenomsClearable.add

added def DenomsClearable

added theorem denomsClearable_C_mul_X_pow

added theorem denomsClearable_natDegree

added theorem denomsClearable_of_natDegree_le

added theorem denomsClearable_zero

added theorem one_le_pow_mul_abs_eval_div