Merge branch 'smooth_bundled_map' of https://github.com/leanprover-co…

…mmunity/mathlib into smooth_bundled_map
leanprover-community · Sep 22, 2020 · 1b61589 · 1b61589
2 parents 5c57c1e + 3e2f3a5
commit 1b61589
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/geometry/manifold/times_cont_mdiff_map.lean b/src/geometry/manifold/times_cont_mdiff_map.lean
@@ -31,8 +31,8 @@ variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 /-- Bundled `n` times continuously differentiable maps. -/
 @[protect_proj]
 structure times_cont_mdiff_map :=
-(to_fun                   : M → M')
-(times_cont_mdiff_to_fun  : times_cont_mdiff I I' n to_fun)
+(to_fun                  : M → M')
+(times_cont_mdiff_to_fun : times_cont_mdiff I I' n to_fun)
 
 /-- Bundled smooth maps. -/
 @[reducible] def smooth_map := times_cont_mdiff_map I I' M M' ⊤