-
Notifications
You must be signed in to change notification settings - Fork 310
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: simple lemmas about polynomials and their degrees (#6220)
This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221). The signature of a theorem changed: ```lean theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (n * m) = p.coeff n ^ m -- <-- the order of the product was `n * m` (p ^ m).coeff (m * n) = p.coeff n ^ m -- <-- and it became `m * n` ``` Modified files: ``` Data/Polynomial/Basic.lean Data/Polynomial/Degree/Lemmas.lean Data/Polynomial/Degree/Definitions.lean Data/Polynomial/Coeff.lean -- for a "`simp` can prove this" golf ```
- Loading branch information
1 parent
43f3be2
commit 769f5fc
Showing
4 changed files
with
30 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters