-
Notifications
You must be signed in to change notification settings - Fork 297
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
refactor(linear_algebra/lc): use families not sets #943
Conversation
a9e1212
to
a7f2a26
Compare
src/linear_algebra/finsupp.lean
Outdated
finsupp.vector_space | ||
/-- Interprets (l : α →₀ γ) as linear combination of the elements in the family (v : α → β) and | ||
evaluates this linear combination. -/ | ||
protected def total : α →₀ γ →ₗ β := finsupp.lsum (λ i, linear_map.id.smul_right (v 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.
alpha and beta can be implicit here
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.
In the expression finsupp.total α β γ v l
, it is very convenient to have the coersion of the linear map finsupp.total α β γ v
into a function. I don't understand why, but if I make alpha and beta implicit, the coersion does no longer work. Any ideas?
435425a
to
4525504
Compare
ee4df40
to
c765545
Compare
f7e57d1
to
7314d88
Compare
7b3de0c
to
167094a
Compare
…ity#943) * refactor(linear_algebra/lc): use families not sets * refactor(linear_algebra/lc): merge lc into finsupp * refactor(linear_algebra/lc): localize decidability * refactor(linear_algebra/lc): finsupp instances * refactor(linear_algebra/lc): use families instead of sets * refactor(linear_algebra/lc): remove set argument in lin_indep * refactor(linear_algebra/lc): clean up * refactor(linear_algebra/lc): more clean up * refactor(linear_algebra/lc): set_option in section * refactor(linear_algebra/lc): decidability proof * refactor(linear_algebra/lc): arrow precedence * refactor(linear_algebra/lc): more cleanup * refactor(linear_algebra/lc): move finset.preimage * refactor(linear_algebra/lc): use families not sets * refactor(linear_algebra/lc): merge lc into finsupp * refactor(linear_algebra/lc): localize decidability * refactor(linear_algebra/lc): finsupp instances * refactor(linear_algebra/lc): use families instead of sets * refactor(linear_algebra/lc): remove set argument in lin_indep * refactor(linear_algebra/lc): clean up * refactor(linear_algebra/lc): more clean up * refactor(linear_algebra/lc): set_option in section * refactor(linear_algebra/lc): decidability proof * refactor(linear_algebra/lc): arrow precedence * refactor(linear_algebra/lc): more cleanup * refactor(linear_algebra/lc): move finset.preimage * tidying up. Remove unnecessary dec_eq from dim. Shorten finset.preimage. * fix build * make travis rebuild * fix build * shorten finsupp proofs * shorten more proofs * shorten more proofs * speed up dim_bot * fix build * shorten dimension proof
I modified the formalization of linear combinations to be based on families instead of sets.
This allows in particular to speak about a family of vectors being linearly dependent if one vector occurs twice.
The old definition is a special case of this new one by using the type of vectors as the index type and the identity as the map of the family.
See also: https://leanprover.zulipchat.com/login/#narrow/stream/116395-maths/topic/linear_independent.20for.20families
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list