Commit 2023-07-19 01:46 801ae802

View on Github →

feat(Tactic/ComputeDegree): add helper lemmas for compute_degree_le (#5978) This PR is a prequel to #5882: it simply adds the helper lemmas about polynomials that the tactic uses. Zulip discussion

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Polynomial/Degree/Definitions.lean

added theorem Polynomial.degree_add_le_of_le

added theorem Polynomial.degree_int_cast_le

added theorem Polynomial.degree_mul_le_of_le

added theorem Polynomial.degree_nat_cast_le

added theorem Polynomial.degree_neg_le_of_le

added theorem Polynomial.degree_pow_le_of_le

added theorem Polynomial.degree_sub_le_of_le

added theorem Polynomial.degree_zero_le

added theorem Polynomial.natDegree_add_le_of_le

added theorem Polynomial.natDegree_mul_le_of_le

added theorem Polynomial.natDegree_neg_le_of_le

added theorem Polynomial.natDegree_pow_le_of_le

added theorem Polynomial.natDegree_sub_le_of_le

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/ComputeDegree.lean

added theorem Mathlib.Tactic.ComputeDegree.natDegree_C_le

added theorem Mathlib.Tactic.ComputeDegree.natDegree_int_cast_le

added theorem Mathlib.Tactic.ComputeDegree.natDegree_nat_cast_le

added theorem Mathlib.Tactic.ComputeDegree.natDegree_one_le

added theorem Mathlib.Tactic.ComputeDegree.natDegree_zero_le