[Merged by Bors] - feat: Matrix.fromRows and Matrix.fromColumns multiplied by vectors
#10379
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
eric-wieser
reviewed
Feb 9, 2024
Comment on lines
147
to
155
| @[simp] | ||
| lemma fromRows_mulVec (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) : | ||
| fromRows A₁ A₂ *ᵥ v = Sum.elim (A₁ *ᵥ v) (A₂ *ᵥ v) := by | ||
| ext (_ | _) <;> rfl | ||
|
|
||
| @[simp] | ||
| lemma vecMul_fromColumns (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) : | ||
| v ᵥ* Matrix.fromColumns B₁ B₂ = Sum.elim (v ᵥ* B₁) (v ᵥ* B₂) := by | ||
| ext (_ | _) <;> rfl |
There was a problem hiding this comment.
Can you also add the ones where the Sum.elim is on the LHS (and the rows/columns are swapped)?
There was a problem hiding this comment.
I didn't know how to prove the other two.
There was a problem hiding this comment.
Where do you get stuck? The proof should be trivial still.
There was a problem hiding this comment.
I committed a sorried lemma. Either provide a proof, or delete it from this PR.
There was a problem hiding this comment.
I pushed a proof; can you add the other lemma?
eric-wieser
reviewed
Feb 9, 2024
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
added
awaiting-author
madvorak
changed the title
Matrix.fromRows_mulVec and Matrix.vecMul_fromColumnsMatrix.fromRows and Matrix.fromColumns multiplied by vectors
madvorak
added
awaiting-review
and removed
awaiting-author
|
bors merge Thanks for this! |
github-actions
bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 9, 2024
#10379) Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20sumType_zeroFun_dotProduct Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Matrix.fromRows and Matrix.fromColumns multiplied by vectorsMatrix.fromRows and Matrix.fromColumns multiplied by vectors
atarnoam
pushed a commit
that referenced
this pull request
Feb 10, 2024
#10379) Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20sumType_zeroFun_dotProduct Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
dagurtomas
pushed a commit
that referenced
this pull request
Mar 22, 2024
#10379) Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20sumType_zeroFun_dotProduct Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
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.
Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20sumType_zeroFun_dotProduct