Mathlib v3 is deprecated. Go to Mathlib v4

Def smooth_within_at

Modification history

2020-07-30 17:59

src/geometry/manifold/times_cont_mdiff.lean

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

Added smooth_within_at View on Github →