New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: port LinearAlgebra.StdBasis #3264
Conversation
Ruben-VandeVelde
commented
Apr 4, 2023
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
exact | ||
funext fun i => | ||
((@supᵢ_pos _ _ _ fun h => range <| std_basis R φ i) <| Finset.mem_univ i).symm | ||
convert top_unique (infᵢ_emptyset.ge.trans <| infᵢ_ker_proj_le_supᵢ_range_stdBasis R φ _) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think convert
might have syntax for naming the variables it intros now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not in the documentation. Let me know what it is if you find it.
Mathlib/LinearAlgebra/StdBasis.lean
Outdated
show (∑ i in I, stdBasis R φ i (b i)) = b by | ||
ext i | ||
rw [Finset.sum_apply, ← stdBasis_same R φ i (b i)] | ||
refine' Finset.sum_eq_single i (fun j hjI ne => stdBasis_ne _ _ _ _ ne.symm _) _ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
One thing that might help here is using refine
instead and replacing only the relevant _
with ?_
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What would this help with?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I already pushed that fix. It tells lean which metavariables it can turn into goals and which it has to solve immediately.
bors merge |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
This PR was included in a batch that was canceled, it will be automatically retried |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com>