Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-30 20:29 bcc7c024

View on Github →

feat(geometry/manifold): smooth bundled maps (#3641)

Estimated changes

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff.mul

added theorem times_cont_diff.smul

modified theorem times_cont_diff_add

added theorem times_cont_diff_at.mul

added theorem times_cont_diff_at.smul

added theorem times_cont_diff_mul

modified theorem times_cont_diff_neg

added theorem times_cont_diff_on.mul

added theorem times_cont_diff_on.smul

added theorem times_cont_diff_smul

added theorem times_cont_diff_within_at.mul

added theorem times_cont_diff_within_at.smul

Renamed src/geometry/algebra/lie_group.lean to src/geometry/manifold/algebra/lie_group.lean

deleted theorem smooth.mul

deleted theorem smooth_left_mul

deleted theorem smooth_mul

deleted theorem smooth_on.mul

deleted theorem smooth_right_mul

Created src/geometry/manifold/algebra/monoid.lean

added structure has_smooth_add_core

added structure has_smooth_mul_core

added theorem smooth.mul

added structure smooth_add_monoid_morphism

added structure smooth_monoid_morphism

added theorem smooth_mul

added theorem smooth_mul_left

added theorem smooth_mul_right

added theorem smooth_on.mul

Created src/geometry/manifold/algebra/smooth_functions.lean

added def smooth_map.C

Created src/geometry/manifold/algebra/structures.lean

Modified src/geometry/manifold/basic_smooth_bundle.lean

Modified src/geometry/manifold/charted_space.lean

Renamed src/geometry/manifold/real_instances.lean to src/geometry/manifold/instances/real.lean

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

deleted theorem smooth_manifold_with_corners.compatible

added theorem smooth_manifold_with_corners_of_times_cont_diff_on

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem smooth.smul

added theorem smooth_smul

Modified src/geometry/manifold/times_cont_mdiff_map.lean

modified theorem times_cont_mdiff_map.coe_inj

modified def times_cont_mdiff_map.comp

modified theorem times_cont_mdiff_map.comp_apply

modified def times_cont_mdiff_map.const

modified def times_cont_mdiff_map.id

Modified src/topology/algebra/continuous_functions.lean

Modified src/topology/algebra/monoid.lean

Modified src/topology/continuous_map.lean

modified def continuous_map.comp

modified def continuous_map.const

Modified src/topology/instances/real.lean

Modified src/topology/path_connected.lean