Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-30 17:59 43ccce55

View on Github →

feat(geometry): first stab on Lie groups (#3529)

Estimated changes

Modified src/algebra/group/defs.lean

added def left_mul

added def right_mul

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff.prod_map

added theorem times_cont_diff_add

added theorem times_cont_diff_at.prod_map'

added theorem times_cont_diff_at.prod_map

added theorem times_cont_diff_at_fst

added theorem times_cont_diff_at_snd

added theorem times_cont_diff_neg

deleted theorem times_cont_diff_on.map_prod

added theorem times_cont_diff_on.prod_map

added theorem times_cont_diff_within_at.prod_map'

added theorem times_cont_diff_within_at.prod_map

added theorem times_cont_diff_within_at_fst

added theorem times_cont_diff_within_at_snd

Modified src/data/equiv/local_equiv.lean

Created src/geometry/algebra/lie_group.lean

added structure lie_add_group_core

added structure lie_add_group_morphism

added structure lie_group_core

added structure lie_group_morphism

added theorem smooth.inv

added theorem smooth.mul

added theorem smooth_inv

added theorem smooth_left_mul

added theorem smooth_mul

added theorem smooth_on.inv

added theorem smooth_on.mul

added theorem smooth_pow

added theorem smooth_right_mul

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

Modified src/geometry/manifold/times_cont_mdiff.lean

added theorem basic_smooth_bundle_core.smooth_at_proj

added theorem basic_smooth_bundle_core.smooth_on_proj

added theorem basic_smooth_bundle_core.smooth_proj

added theorem basic_smooth_bundle_core.smooth_within_at_proj

added theorem basic_smooth_bundle_core.times_cont_mdiff_at_proj

added theorem basic_smooth_bundle_core.times_cont_mdiff_on_proj

added theorem basic_smooth_bundle_core.times_cont_mdiff_proj

added theorem basic_smooth_bundle_core.times_cont_mdiff_within_at_proj

added theorem smooth.comp_smooth_on

added theorem smooth.prod_map

added theorem smooth.prod_mk

added theorem smooth.smooth_at

added theorem smooth.smooth_on

added theorem smooth.times_cont_mdiff

added def smooth

added theorem smooth_at.prod_map

added theorem smooth_at.prod_mk

added theorem smooth_at.smooth_within_at

added theorem smooth_at.times_cont_mdiff_at

added def smooth_at

added theorem smooth_at_const

added theorem smooth_at_fst

added theorem smooth_at_id

added theorem smooth_at_snd

added theorem smooth_at_univ

added theorem smooth_const

added theorem smooth_fst

added theorem smooth_id

added theorem smooth_iff

added theorem smooth_iff_proj_smooth

added theorem smooth_on.prod_map

added theorem smooth_on.prod_mk

added theorem smooth_on.times_cont_mdiff_on

added def smooth_on

added theorem smooth_on_const

added theorem smooth_on_fst

added theorem smooth_on_id

added theorem smooth_on_iff

added theorem smooth_on_snd

added theorem smooth_on_univ

added theorem smooth_snd

added theorem smooth_within_at.prod_map

added theorem smooth_within_at.prod_mk

added theorem smooth_within_at.smooth_at

added theorem smooth_within_at.times_cont_mdiff_within_at

added def smooth_within_at

added theorem smooth_within_at_const

added theorem smooth_within_at_fst

added theorem smooth_within_at_id

added theorem smooth_within_at_iff

added theorem smooth_within_at_snd

added theorem tangent_bundle.smooth_at_proj

added theorem tangent_bundle.smooth_on_proj

added theorem tangent_bundle.smooth_proj

added theorem tangent_bundle.smooth_within_at_proj

added theorem tangent_bundle.times_cont_mdiff_at_proj

added theorem tangent_bundle.times_cont_mdiff_on_proj

added theorem tangent_bundle.times_cont_mdiff_proj

added theorem tangent_bundle.times_cont_mdiff_within_at_proj

added theorem times_cont_mdiff.comp_times_cont_mdiff_on

added theorem times_cont_mdiff.prod_map

added theorem times_cont_mdiff.prod_mk

added theorem times_cont_mdiff.smooth

modified theorem times_cont_mdiff_at.comp

added theorem times_cont_mdiff_at.prod_map'

added theorem times_cont_mdiff_at.prod_map

added theorem times_cont_mdiff_at.prod_mk

added theorem times_cont_mdiff_at.smooth_at

added theorem times_cont_mdiff_at_fst

added theorem times_cont_mdiff_at_snd

added theorem times_cont_mdiff_fst

added theorem times_cont_mdiff_on.prod_map

added theorem times_cont_mdiff_on.prod_mk

added theorem times_cont_mdiff_on.smooth_on

added theorem times_cont_mdiff_on_fst

added theorem times_cont_mdiff_on_snd

added theorem times_cont_mdiff_snd

modified theorem times_cont_mdiff_within_at.comp'

modified theorem times_cont_mdiff_within_at.comp

added theorem times_cont_mdiff_within_at.prod_map'

added theorem times_cont_mdiff_within_at.prod_map

added theorem times_cont_mdiff_within_at.prod_mk

added theorem times_cont_mdiff_within_at.smooth_within_at

added theorem times_cont_mdiff_within_at_fst

added theorem times_cont_mdiff_within_at_iff

added theorem times_cont_mdiff_within_at_snd

Modified src/topology/continuous_on.lean

added theorem continuous_on_fst

added theorem continuous_on_snd

added theorem continuous_within_at_fst

added theorem continuous_within_at_snd

added theorem nhds_within_prod