[Merged by Bors] - feat(algebra/module/submodule): add smul_of_tower_mem
#6712
Conversation
| convert (L m).has_fderiv_at.comp_has_fderiv_within_at x this }, | ||
| -- `convert (L m).has_fderiv_at.comp_has_fderiv_within_at x this` no longer works. | ||
| convert has_fderiv_at.comp_has_fderiv_within_at x _ this, | ||
| rotate 2, | ||
| convert linear_isometry_equiv.has_fderiv_at _, | ||
| rotate 1, | ||
| convert L m using 1, | ||
| refl, | ||
| refl, }, |
There was a problem hiding this comment.
I can't work out what's going on here - (L m).has_fderiv_at is now a type error, but it's very difficult for me to work out which bits of the types mismatch.
There was a problem hiding this comment.
Maybe you already fixed it? When I change it back to check the error, I don't get an error.
There was a problem hiding this comment.
Are you sure you had the right cache loaded? I tested this in the last commit it was still broken.
There was a problem hiding this comment.
I am relatively sure. Maybe it's a lean 3.27 / lean 3.28 issue?
% git status
On branch eric-wieser/smul_mem_of_tower
Your branch is up to date with 'mathlib/eric-wieser/smul_mem_of_tower'.
% git pull
Already up to date.
% leanproject get-cache
Looking for local mathlib oleans
Found local mathlib oleans
% lean --make src/analysis/calculus/times_cont_diff.lean
% lean --version
Lean (version 3.27.0, commit de35266fe596, Release)
There was a problem hiding this comment.
I pushed commit 659086a to a new branch, let's see what CI thinks.
There was a problem hiding this comment.
Seems to work? Perhaps I was running into another hash collision?
There was a problem hiding this comment.
The commit passed the build stage, so can you merge it back into your branch?
There was a problem hiding this comment.
Done. Thanks for double-checking this, I probably screwed up somehow when I did.
eric-wieser
added
the
awaiting-review
|
Thanks! bors r+ |
github-actions
bot
added
ready-to-merge
This adds the lemmas: * `sub_mul_action.smul_of_tower_mem` * `submodule.smul_of_tower_mem` And uses them to construct the new scalar actions: * `sub_mul_action.mul_action'` * `sub_mul_action.is_scalar_tower` * `submodule.semimodule'` * `submodule.is_scalar_tower` With associated lemmas * `sub_mul_action.coe_smul_of_tower` * `submodule.coe_smul_of_tower` The unprimed instance continue to hold their old values, and exist to speed up typeclass search; the same pattern we use for `tensor_product.semimodule` vs `tensor_product.semimodule`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
smul_of_tower_memsmul_of_tower_mem
This adds the lemmas: * `sub_mul_action.smul_of_tower_mem` * `submodule.smul_of_tower_mem` And uses them to construct the new scalar actions: * `sub_mul_action.mul_action'` * `sub_mul_action.is_scalar_tower` * `submodule.semimodule'` * `submodule.is_scalar_tower` With associated lemmas * `sub_mul_action.coe_smul_of_tower` * `submodule.coe_smul_of_tower` The unprimed instance continue to hold their old values, and exist to speed up typeclass search; the same pattern we use for `tensor_product.semimodule` vs `tensor_product.semimodule`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
This adds the lemmas:
sub_mul_action.smul_of_tower_memsubmodule.smul_of_tower_memAnd uses them to construct the new scalar actions:
sub_mul_action.mul_action'sub_mul_action.is_scalar_towersubmodule.semimodule'submodule.is_scalar_towerWith associated lemmas
sub_mul_action.coe_smul_of_towersubmodule.coe_smul_of_towerThe unprimed instance continue to hold their old values, and exist to speed up typeclass search; the same pattern we use for
tensor_product.semimodulevstensor_product.semimodule.Split from #5569, which opened a can of elaborator-weakening worms that broke every call site of
submodule.smul_mem. It's easier to just add a new lemma,smul_mem_of_tower, and leave combining the lemmas into a single lemma for another time. We already do things this way for linear_map anyway.A natural follow-up here is to ensure that the
Z-module structure from #5430 gets transferred too, but I'm going to punt that to another time.