Commit 2021-03-07 10:18 02251b1e

refactor(geometry/manifold): drop some unused arguments (#6545) API changes:

• add lemmas about map (ext_chart_at I x) (𝓝[s] x');
• prove times_cont_mdiff_within_at.comp directly without using other charts; the new proof does not need a smooth_manifold_with_corners instance;
• add aliases times_cont_mdiff.times_cont_diff etc;
• times_cont_mdiff_map no longer needs a smooth_manifold_with_corners instance;
• has_smooth_mul no longer extends smooth_manifold_with_corners and no longer takes has_continuous_mul as an argument;
• has_smooth_mul_core is gone in favor of has_continuous_mul_of_smooth;
• smooth_monoid_morphism now works with any model space (needed, e.g., to define smooth_monoid_morphism.prod);
• lie_group_morphism is gone: we use M →* N both for monoids and groups, no reason to have two structures in this case;
• lie_group no longer extends smooth_manifold_with_corners and no longer takes topological_group as an argument;
• lie_group_core is gone in favor of topological_group_of_lie_group;
• the I : model_with_corners 𝕜 E H argument of smooth_mul and smooth_inv is now explicit.