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(linear_algebra): determinant of vectors in a basis #3919
Conversation
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.
Thanks 🎉
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
Also renames `equiv_fun_basis` to `is_basis.equiv_fun` in order to use dot notation.
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.
Thanks for the work! Since I co-authored some of the definitions, I'll invite someone else to take a look as well.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Thanks @robertylewis! |
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'm not too familiar with the linear algebra part of the library, but this looks good to me.
I do agree that linear_algebra/matrix.lean
does need to be cleaned up or split up into multiple files. The file could also use sectioning module doc strings.
src/linear_algebra/basic.lean
Outdated
@@ -1709,6 +1709,9 @@ rfl | |||
@[simp] theorem map_zero : e 0 = 0 := e.to_linear_map.map_zero | |||
@[simp] theorem map_smul (c : R) (x : M) : e (c • x) = c • e x := e.map_smul' c x | |||
|
|||
@[simp] lemma map_sum [fintype ι] (u : ι → M) : e (∑ i, u i) = ∑ i, e (u i) := |
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.
Shouldn't this rather be done more generally for sums over finsets?
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Thanks 🎉 bors merge |
From the sphere eversion project, define the determinant of a family of vectors with respects to a basis. The main result is `is_basis.iff_det` asserting a family of vectors is a basis iff its determinant in some basis is invertible. Also renames `equiv_fun_basis` to `is_basis.equiv_fun` and `equiv_fun_basis_symm_apply` to `is_basis.equiv_fun_symm_apply`, in order to use dot notation. Co-authored-by: Anne Baanen t.baanen@vu.nl Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Pull request successfully merged into master. Build succeeded: |
From the sphere eversion project, define the determinant of a family of vectors with respects to a basis. The main result is `is_basis.iff_det` asserting a family of vectors is a basis iff its determinant in some basis is invertible. Also renames `equiv_fun_basis` to `is_basis.equiv_fun` and `equiv_fun_basis_symm_apply` to `is_basis.equiv_fun_symm_apply`, in order to use dot notation. Co-authored-by: Anne Baanen t.baanen@vu.nl Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
From the sphere eversion project, define the determinant of a family of vectors with respects to a basis.
The main result is
is_basis.iff_det
asserting a family of vectors is a basis iff its determinant in some basis is invertible.Also renames
equiv_fun_basis
tois_basis.equiv_fun
andequiv_fun_basis_symm_apply
tois_basis.equiv_fun_symm_apply
, in order to use dot notation.Co-authored-by: Anne Baanen t.baanen@vu.nl
Note that this file
linear_algebra.matrix
is becoming a mess. We should probably move a few things and add headers, but I didn't want to do this and add content at the same time (and also I'm toolazybusy right now).