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: Invertible matrices #8219
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
simp_rw [vecMul_transpose] | ||
exact LinearMap.surjective_of_injective (f := A.mulVecLin) h | ||
change Function.Injective A.mulVecLin | ||
rw [←LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'] |
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.
rw [←LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'] | |
rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'] |
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.
Is there a style guide reference for having the space after the arrow?
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.
And if it's part of the official style, why doesn't the linter enforce it?
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.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
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.
bors merge
Thanks, and sorry for letting this fall off my radar
We add some results on invertible matrices, showing that for a finite square matrix `A`, `IsUnit A` is equivalent to the surjectivity/injectivity of left/right multiplication, and to the linear independence of the set of rows/columns. We also add a couple of lemmas about the existence of left/right inverses for nonsquare matrices, and a bit of API for `mulVecLin` and `vecMulLinear`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
We add some results on invertible matrices, showing that for a finite square matrix `A`, `IsUnit A` is equivalent to the surjectivity/injectivity of left/right multiplication, and to the linear independence of the set of rows/columns. We also add a couple of lemmas about the existence of left/right inverses for nonsquare matrices, and a bit of API for `mulVecLin` and `vecMulLinear`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
We add some results on invertible matrices, showing that for a finite square matrix
A
,IsUnit A
is equivalent to the surjectivity/injectivity of left/right multiplication, and to the linear independence of the set of rows/columns.We also add a couple of lemmas about the existence of left/right inverses for nonsquare matrices, and a bit of API for
mulVecLin
andvecMulLinear
.