[Merged by Bors] - feat: Dual basis of power basis wrt trace form #8835
Conversation
erdOne
commented
Dec 6, 2023
erdOne
commented
erdOne
added
awaiting-review
|
It looks still good to me, thanks! bors merge |
|
bors r- |
|
Canceled. |
github-actions
bot
added
ready-to-merge
|
Sorry, I was working on another PR and I switched tab. |
erdOne
added
awaiting-review
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
leanprover-community-mathlib4-bot
added
the
merge-conflict
|
Can you please fix the conflict? |
…lib4 into erd1/minpolyDiv
leanprover-community-mathlib4-bot
removed
the
merge-conflict
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
| lemma coeff_minpolyDiv_sub_pow_mem_span {i} (hi : i ≤ natDegree (minpolyDiv R x)) : | ||
| coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i ∈ | ||
| Submodule.span R ((x ^ ·) '' Set.Iio i) := by |
There was a problem hiding this comment.
I created #9071 which may make some lemmas easier, including this.
There was a problem hiding this comment.
I failed to use them to make the proofs shorter.
There was a problem hiding this comment.
I'll try later. I think several lemmas could be easier using what we know about divByMonic, instead of using the characterization you introduced.
I've started wondering whether we should prove something general about upper/lower triangular matrices (with 1 on the diagonal) or such linear systems ... but #9071 was merged really quickly (thanks!)
Edit: sorry there's probably nothing general. It's about the inverse of a particular type of bidiagonal matrix. There exists a general formula for the inverse of bidiagonal matrices, but it's probably too complicated for the use case here.
It might help to prove the stronger statement that the submodule spanned by the first i coefficients is equal to that spanned by the first i powers of x.
…lib4 into erd1/minpolyDiv
…nity/mathlib4 into erd1/minpolyDiv
|
What's the status of this PR? I suggest we merge it first and golf it later as the proofs are already not that long. |
|
I agree, we can golf it later. Thanks! bors merge |
github-actions
bot
added
ready-to-merge
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
