refactor(linear_algebra/lc): use families not sets #943
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
abentkamp
force-pushed
the
linear_independent
branch
from
a9e1212
to
a7f2a26
Compare
jcommelin
reviewed
Apr 17, 2019
digama0
reviewed
Apr 19, 2019
digama0
reviewed
Apr 19, 2019
digama0
reviewed
Apr 19, 2019
digama0
reviewed
Apr 19, 2019
digama0
reviewed
Apr 19, 2019
digama0
reviewed
Apr 19, 2019
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.
alpha and beta can be implicit here
There was a problem hiding this comment.
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?
abentkamp
force-pushed
the
linear_independent
branch
2 times, most recently
from
435425a
to
4525504
Compare
abentkamp
force-pushed
the
linear_independent
branch
4 times, most recently
from
ee4df40
to
c765545
Compare
digama0
reviewed
Jun 20, 2019
digama0
reviewed
Jun 20, 2019
digama0
reviewed
Jun 20, 2019
digama0
reviewed
Jun 20, 2019
digama0
reviewed
Jun 20, 2019
abentkamp
force-pushed
the
linear_independent
branch
2 times, most recently
from
f7e57d1
to
7314d88
Compare
digama0
reviewed
Jun 21, 2019
abentkamp
force-pushed
the
linear_independent
branch
from
7b3de0c
to
167094a
Compare
digama0
approved these changes
Jul 3, 2019
ChrisHughes24
added
the
ready-to-merge
anrddh
pushed a commit
to anrddh/mathlib
that referenced
this pull request
May 15, 2020
…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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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