Commit 2019-12-17 14:48 d8dc1445
View on Github →feat(geometry/manifold): smooth bundles, tangent bundle (#1607)
- feat(geometry/manifold): smooth bundles, tangent bundle
- remove decidable in preamble
- Update src/geometry/manifold/basic_smooth_bundle.lean Co-Authored-By: Johan Commelin johan@commelin.net
- Update src/geometry/manifold/basic_smooth_bundle.lean Co-Authored-By: Johan Commelin johan@commelin.net
- Update src/geometry/manifold/basic_smooth_bundle.lean Co-Authored-By: Johan Commelin johan@commelin.net
- comments
- cleanup
- oops, forgot squeeze_simp
- simpa instead of simp
- oops
- much better docstrings
- improved formatting
- space after forall
- fix build
- fix build, continuous.smul
- minor improvements