feat: define C^n submersions (leanprover-community#35122)

This PR defines submersions between C^n manifolds. In the infinite-dimensional setting, submersions are defined via local normal forms rather than surjectivity of the mfderiv. A map f is a submersion at x if, in suitable charts around x and f x, it has the form (u, v) ↦ u after identifying the model space with a product.

We prove a few basic properties:
- being a submersion is a local property,
- products of submersions are submersions,
- the set of submersed points is open

Future PRs will prove that submersions are C^n and deduce equivalence with the standard definition in finite dimensions. From the path towards the regular value theorem.

This file was developed under the supervision of Michael Rothgang.

Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Samantha M. Naranjo <naranjosamantha1j@gmail.com>
Co-authored-by: Samantha Naranjo <naranjosamantha1j@gmail.com>

Author: Marygold-Dusk

Mathlib.lean

@@ -4679,6 +4679,7 @@ public import Mathlib.Geometry.Manifold.Sheaf.Smooth
 public import Mathlib.Geometry.Manifold.SmoothApprox
 public import Mathlib.Geometry.Manifold.SmoothEmbedding
 public import Mathlib.Geometry.Manifold.StructureGroupoid
+public import Mathlib.Geometry.Manifold.Submersion
 public import Mathlib.Geometry.Manifold.VectorBundle.Basic
 public import Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
 public import Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic