Commit 2024-03-15 10:37 2a70469b

View on Github →

feat: add lemmas Polynomial.natDegree_sum_le_of_forall_le (#11381) Also add two missing simp attributes

Estimated changes

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

added theorem Polynomial.natDegree_sum_le_of_forall_le

Modified Mathlib/Data/Fin/Basic.lean

modified theorem Fin.cast_val_eq_self

Modified Mathlib/Data/Polynomial/Basic.lean