Mathlib Changelog
v3
Changelog
About
Github
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