[Merged by Bors] - feat: add a few analytic function lemmas for future AnalyticManifold use#13784
[Merged by Bors] - feat: add a few analytic function lemmas for future AnalyticManifold use#13784
Conversation
This is a few isolated lemmas split out of #10853. 1. AnalyticAt.comp_of_eq 2. FormalMultilinearSeries.zero_radius 3. constFormalMultilinearSeries_zero
PR summary e7397798a3Import changesNo significant changes to the import graph Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
grunweg
left a comment
There was a problem hiding this comment.
Thanks for splitting this out. This looks good to me - re-reviewing, I just have one question about generalisation.
| (by simp [constFormalMultilinearSeries]) | ||
| #align formal_multilinear_series.const_formal_multilinear_series_radius FormalMultilinearSeries.constFormalMultilinearSeries_radius | ||
|
|
||
| /-- `0` has infinite radius of convergence -/ |
There was a problem hiding this comment.
Does this generalise to any constant formal series?
There was a problem hiding this comment.
Not really, as this is the 0 of that type, not an injection from the field 0.
| Nat.casesOn n (fun hn => (hn rfl).elim) (fun _ _ => rfl) hn | ||
| #align const_formal_multilinear_series_apply constFormalMultilinearSeries_apply | ||
|
|
||
| @[simp] |
There was a problem hiding this comment.
Can you generalise this to any c : F (or am I misunderstanding how FormatMultilinearSeries works)?
There was a problem hiding this comment.
This is saying the injection from the field commutes with Zero, so I don’t think it sensibly generalizes.
|
Are there changes I should make? I think I’ve replied to comments above, but in the past I’ve messed up the UI and comments didn’t get posted, so I want to make sure. |
|
No worries, I saw your comments. Right now, I don't have the time to wrap my head around your comments in detail - but what you say sounds reasonable, so let me |
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
This is a few isolated lemmas split out of
#10853.