[Merged by Bors] - chore(LinearAlgebra/TensorProduct/Basic): semi-linearize map and lift#27288
[Merged by Bors] - chore(LinearAlgebra/TensorProduct/Basic): semi-linearize map and lift#27288themathqueen wants to merge 15 commits intoleanprover-community:masterfrom
map and lift#27288Conversation
PR summary 652dbc72e5Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
My slight preference here would be to push forward with at least parts of #24208 |
@eric-wieser I agree, but I still think (and I think @ADedecker would agree) that we should create duplicate definitions for a lot of the things, including |
|
My conclusion was indeed that some things need to be duplicated, but I don't think this is the case for |
map and liftmap and lift
|
@eric-wieser, mind taking a look at this? It's part of #27353, but for the stuff that doesn't depend on the refactor of |
map and liftmap and lift
|
Shouldn't we also upgrade |
That's part of the next PR #27353 (with a lot more semilinearizing). I guess it won't hurt to do |
|
@themathqueen I'm getting mixed signals from your labeling and comments: are you planning to handle I'm adding back |
|
I initially thought it wouldn't hurt to do. But I'd rather leave it for the next PR, because then we'd also need to semilinearize |
|
OK let's go with this then. Thanks! bors merge |
…ift` (#27288) Semi-linearizing `TensorProduct.map`. This is important as we can then define `star` on tensors as: `star x := map (starLinearEquiv R) (starLinearEquiv R) x`. We can then also define the inner product on tensors. Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
map and liftmap and lift
…ift` (leanprover-community#27288) Semi-linearizing `TensorProduct.map`. This is important as we can then define `star` on tensors as: `star x := map (starLinearEquiv R) (starLinearEquiv R) x`. We can then also define the inner product on tensors. Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
…ift` (leanprover-community#27288) Semi-linearizing `TensorProduct.map`. This is important as we can then define `star` on tensors as: `star x := map (starLinearEquiv R) (starLinearEquiv R) x`. We can then also define the inner product on tensors. Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
…ift` (leanprover-community#27288) Semi-linearizing `TensorProduct.map`. This is important as we can then define `star` on tensors as: `star x := map (starLinearEquiv R) (starLinearEquiv R) x`. We can then also define the inner product on tensors. Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Semi-linearizing
TensorProduct.map. This is important as we can then definestaron tensors as:star x := map (starLinearEquiv R) (starLinearEquiv R) x. We can then also define the inner product on tensors.Co-authored-by: Anatole Dedecker anatolededecker@gmail.com
Part of #27353.