Commit 2021-01-23 13:02 3a136f81

View on Github →

refactor(analysis/analytic/composition): extend definition, extract a lemma from a proof (#5850) Extract a standalone lemma of the proof that the composition of two analytic functions is well-behaved, and extend a little bit the definition of the sets which are involved in the corresponding change of variables.

Estimated changes

Modified src/analysis/analytic/composition.lean

modified def formal_multilinear_series.comp_change_of_variables

added theorem formal_multilinear_series.comp_change_of_variables_sum

modified def formal_multilinear_series.comp_partial_sum_source

modified def formal_multilinear_series.comp_partial_sum_target

modified def formal_multilinear_series.comp_partial_sum_target_set

modified theorem formal_multilinear_series.mem_comp_partial_sum_source_iff

modified theorem formal_multilinear_series.mem_comp_partial_sum_target_iff