mathlib
0dc40792 - refactor(geometry/manifold/cont_mdiff_map): refactor to reduce imports (#19164)

Commit
2 years ago
refactor(geometry/manifold/cont_mdiff_map): refactor to reduce imports (#19164) See https://tqft.net/mathlib4/2023-06-07/geometry.manifold.algebra.left_invariant_derivation.pdf for the motivation. I'm happy if this one is shot down. :-) Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Author
Parents
Loading