Mr. Covariant Derivatives

[grunweg]

This PR is a work in progress, and will land in individual pieces. Some contributions include

• additional API for differentiability of vector bundle sections
• finite sums, differences and scalar products of smooth sections are smooth
• the same result for mdifferentiable
• add missing mdifferentiable congruence lemmas
• define smooth local frames of a vector bundle
• a general tensoriality criterion
• define covariant derivatives, proving their tensoriality and that convex combinations of these are covariant derivatives
• the classification of covariant derivatives over a trivial bundle
• additional API for the Lie bracket of vector fields: the product rule (one sorry left!), Lie bracket at zero vanishes
• torsion of a connection, torsion-free connections
• Gram-Schmidt procedure for sections of a Riemannian vector bundle
• orthonormal frames on a Riemannian vector bundle
• connections compatible with a metric; definition of the Levi-Civita connection
• uniqueness of the Levi-Civita connection
• Christoffel symbols
• in progress: existence of the Levi-Civita connection (connection done; torsion-freeness and compatibility in progress)
• custom elaborators for sections in a vector bundle (converting dependent to non-dependent functions)
• custom elaborators for inferring a model with corners, in differentiability/smoothness definitions
• a #check' command and tactic which only shows explicit arguments

More to come soon!

Joint work with @PatrickMassot; supported by the FMJH.

---

• depends on: [Merged by Bors] - feat: add lemma mdifferentiableAt_totalSpace #26360
• depends on: [Merged by Bors] - feat: add continuousOn_iUnion #26672
• depends on: [Merged by Bors] - feat: contMDiffOn_iUnion_iff_of_isOpen #26673
• depends on: [Merged by Bors] - feat: finite sum, difference, scalar product of C^k sections is C^k #26674
• depends on: [Merged by Bors] - chore(VectorBundle/Basic): minor clean-ups and polish #26864 (more of a by-product)
• depends on: [Merged by Bors] - feat(VectorBundle/MDifferentiable): add some basic API #26865
• depends on: [Merged by Bors] - feat(VectorBundle/MDifferentiable): differentiability results for coordChange #26866
• depends on: [Merged by Bors] - feat: mdifferentiableOn_section_of_mem_baseSet₀ #26870
• depends on: [Merged by Bors] - feat: finite sum, difference, scalar product of differentiable sections is differentiable #26871
• depends on: [Merged by Bors] - feat: contMDiff_section_of_tsupport #26671
• depends on: [Merged by Bors] - feat: contMDiffWithinAt_zeroSection #26676
• depends on: [Merged by Bors] - chore(Geometry/Manifold/VectorBundle/Basic): make some arguments implicit #26677
• depends on: [Merged by Bors] - feat: contMDiffOn_section_of_mem_baseSet #26678
• depends on: [Merged by Bors] - feat: DifferentiableOn.iUnion #26686
• depends on: [Merged by Bors] - feat: MDifferentiableOn.iUnion #26687
• depends on: [Merged by Bors] - feat: ContDiffOn.iUnion #26688
• depends on: [Merged by Bors] - feat: add missing API for MDifferentiable*.{add,neg} #26702
• depends on: [Merged by Bors] - feat: missing congruence lemmas for mdifferentiability #26709
• depends on: [Merged by Bors] - feat: Lie bracket with zero is zero #26734
• depends on: [Merged by Bors] - feat: product rule for Lie bracket on manifolds #26743
• depends on: [Merged by Bors] - chore(Gram-Schmidt): small tweaks #26894
• depends on: [Merged by Bors] - feat: add mdifferentiable analogues of C^n metric lemmas #26921
• depends on: [Merged by Bors] - feat: add mdifferentiable version of hom bundle smoothness lemmas #26922
• depends on: feat: Finite.linearOrder, choosing *some* linear order on a finite type #27020
• depends on: [Merged by Bors] - feat: custom elaborators for differential geometry #27021
• depends on: [Merged by Bors] - feat: support coercions in the differential geometry elaborators #30307
• depends on: [Merged by Bors] - feat: gramSchmidtNormed_linearIndependent and minor tweaks #27023
• depends on: feat: Gram-Schmidt orthonormalisation for sections of a vector bundle #27024
• depends on: feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections #27025
• depends on: [Merged by Bors] - feat: local frames in a vector bundle #30338
• depends on: [Merged by Bors] - feat: local frames in a vector bundle #30083
• depends on: feat: extend a tangent vector for a locally smooth vector field #30339
• depends on: [Merged by Bors] - feat: add #check' command and tactic, which only show explicit arguments #31194
• depends on: feat: add mfderiv_const_smul #34262
• depends on: [Merged by Bors] - feat: mfderiv_smul #34263

[github-actions]

PR summary 7c0aa26a8b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.VectorField.LieBracket	1
Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.VectorField.Pullback	2
4 files Mathlib.Geometry.Manifold.Riemannian.Basic Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Riemannian	3
Mathlib.Geometry.Manifold.VectorBundle.Misc (new file)	2242
Mathlib.Geometry.Manifold.VectorBundle.GramSchmidtOrtho (new file)	2319
Mathlib.Geometry.Manifold.VectorBundle.OrthonormalFrame (new file)	2321
Mathlib.Geometry.Manifold.VectorBundle.Tensoriality (new file)	2560
Mathlib.Geometry.Manifold.Riemannian.ExistsRiemannianMetric (new file)	2574
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Prelim (new file)	2578
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic (new file)	2579
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion (new file)	2580
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Lift (new file)	2581
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita (new file)	2585

---

Declarations diff

+ Bundle.Trivial.mdifferentiableAt_iff
+ Bundle.pullback_diag
+ Bundle.torsion
+ ChristoffelSymbol
+ ChristoffelSymbol.sum_eq
+ ContMDiff.smul_section_of_tsupport'
+ ContMDiffCovariantDerivative
+ ContMDiffCovariantDerivative.affineCombination
+ ContMDiffCovariantDerivative.affineCombination'
+ ContMDiffCovariantDerivativeOn
+ ContMDiffWithinAt.orthogonalProjection
+ CovariantDerivative
+ CovariantDerivative.geodVF
+ CovariantDerivative.geodVF_horiz
+ CovariantDerivative.isGeod
+ CovariantDerivative.isGeodAt
+ CovariantDerivative.isGeodAt_iff_horiz
+ CovariantDerivative.isGeodAt_iff_proj
+ CovariantDerivative.lift_vec
+ CovariantDerivative.lift_vec_apply
+ CovariantDerivative.lift_vec_eq
+ CovariantDerivative.lift_vec_eq_iff
+ CovariantDerivative.lift_vec_horiz
+ CovariantDerivative.mfderiv_proj_lift_vec
+ CovariantDerivative.orbit_geodVF
+ CovariantDerivative.proj_geodVF
+ CovariantDerivative.proj_lift_vec
+ FiberBundle.trivializationAt.baseSet_mem_nhds
+ IsBilinearMap
+ IsBilinearMap.toContinuousLinearMap
+ IsBilinearMap.toLinearMap
+ IsCompatible
+ IsCovariantDerivativeOn
+ IsCovariantDerivativeOn.fst_comp_lift_vec
+ IsCovariantDerivativeOn.lift_vec
+ IsCovariantDerivativeOn.lift_vec_apply
+ IsCovariantDerivativeOn.lift_vec_eq_iff
+ IsCovariantDerivativeOn.projection_lift_vec
+ IsLeviCivitaConnection
+ IsLeviCivitaConnection.eq_leviCivitaRhs
+ IsLeviCivitaConnection.uniqueness
+ IsLocalFrameOn.gramSchmidtNormed
+ IsMIntegralCurveAt.acceleration
+ IsMIntegralCurveAt.eventually_acceleration
+ IsMIntegralCurveAt.eventually_isMIntegralCurveAt
+ IsMIntegralCurveAt.mdifferentiableAt
+ IsMIntegralCurveAt.mfderiv
+ IsMIntegralCurveAt.proj_acceleration
+ IsMIntegralCurveAt.velocity_eventuallyEq
+ IsMIntegralCurveAt_iff_mfderiv
+ IsOrthonormalFrameOn
+ IsOrthonormalFrameOn.gramSchmidtNormed
+ IsOrthonormalFrameOn.mono
+ IsTorsionFree
+ IsTorsionFreeOn
+ LeviCivitaConnection
+ LeviCivitaConnection.christoffelSymbol_symm
+ LeviCivitaConnection_aux
+ LinearEquiv.comap_isCompl
+ LinearMap.comap_isCompl
+ MDifferentiable.inner_bundle'
+ MDifferentiableAt.inner_bundle'
+ V
+ W
+ _root_.Bundle.vert
+ _root_.ContMDiffCovariantDerivativeOn.affineCombination
+ _root_.ContMDiffCovariantDerivativeOn.affineCombination'
+ _root_.CovariantDerivative.exists_one_form
+ _root_.IsCovariantDerivativeOn.congr_iff_christoffelSymbol_eq
+ _root_.IsCovariantDerivativeOn.congr_of_christoffelSymbol_eq
+ _root_.IsCovariantDerivativeOn.isTorsionFreeOn_iff_localFrame
+ _root_.contMDiffAt_orthonormalFrame_of_mem
+ _root_.mdifferentiableAt_orthonormalFrame_of_mem
+ _root_.mdifferentiableAt_section_trivial_iff
+ add_one_form
+ apply_section_eventuallyEq
+ apply_symm_eventuallyEq
+ aux1
+ aux2
+ aux_computation
+ aux_computation2
+ aux_computation2'
+ aux_special
+ aux_tvs
+ bar
+ baseSet_mem_nhds
+ baseSet_prod_univ_mem_nhds
+ baz
+ bijective_deriv
+ bijective_symm
+ christoffelSymbol_zero
+ christoffelSymbol_zero_apply
+ coe_gramSchmidtBasis
+ coe_gramSchmidtNormedBasis
+ coeff_eq_inner'
+ comap_trivializationAt_horiz
+ comap_vert
+ comp_invFun_eventuallyEq
+ condition
+ condition1
+ condition2
+ congr_X_at
+ congr_of_forall_product
+ congr_σ_of_eqOn
+ congr_σ_smoothBumpFunction
+ contDiff_extend
+ contMDiffAt_aux
+ contMDiffAt_coeff
+ contMDiffAt_iff_coeff
+ contMDiffAt_iff_coeff'
+ contMDiffCovariantDerivativeOn_univ_iff
+ contMDiffOn_coeff
+ contMDiffOn_iff_coeff
+ contMDiffOn_iff_coeff'
+ contMDiffOn_localExtensionOn
+ contMDiffOn_orthonormalFrame_baseSet
+ contMDiffWithinAt_aux
+ contMDiffWithinAt_coeff
+ contMDiffWithinAt_inner
+ contMDiff_extend
+ contMDiff_localSection
+ convex_condition
+ convex_condition1
+ convex_condition2
+ coordChangeL_coordChangeL
+ coordChangeL_mem_horiz
+ coordChangeL_mem_horiz_iff
+ coordChangeL_pushCovDer
+ cov_eq_proj
+ deriv
+ derivInv
+ derivInv_deriv
+ derivInv_deriv_apply
+ deriv_derivInv
+ deriv_derivInv_apply
+ difference
+ differenceAux
+ differenceAux_apply
+ differenceAux_smul_eq
+ differenceAux_smul_eq'
+ differenceAux_tensorial
+ difference_apply
+ difference_def
+ eq_of
+ eq_one_form
+ eq_product_apply
+ evalL
+ exists_map_of
+ exists_one_form
+ extend
+ extend_add
+ extend_apply_self
+ extend_smul
+ extend_zero
+ foo
+ foo_aux
+ foo_aux_prop
+ foobar
+ fst_comp_eventuallyEq
+ gramSchmidt
+ gramSchmidtBasis
+ gramSchmidtNormed
+ gramSchmidtNormedBasis
+ gramSchmidtNormed_apply_of_orthogonal
+ gramSchmidtNormed_apply_of_orthonormal
+ gramSchmidtNormed_coe
+ gramSchmidtNormed_contMDiff
+ gramSchmidtNormed_contMDiffAt
+ gramSchmidtNormed_contMDiffOn
+ gramSchmidtNormed_contMDiffWithinAt
+ gramSchmidtNormed_linearIndependent
+ gramSchmidtNormed_orthonormal
+ gramSchmidtNormed_orthonormal'
+ gramSchmidtNormed_unit_length
+ gramSchmidtNormed_unit_length'
+ gramSchmidtNormed_unit_length_coe
+ gramSchmidtOrthonormalBasis
+ gramSchmidtOrthonormalBasis_apply_of_orthonormal
+ gramSchmidtOrthonormalBasis_coe
+ gramSchmidt_apply
+ gramSchmidt_bot
+ gramSchmidt_contMDiff
+ gramSchmidt_contMDiffAt
+ gramSchmidt_contMDiffOn
+ gramSchmidt_contMDiffWithinAt
+ gramSchmidt_def
+ gramSchmidt_def'
+ gramSchmidt_def''
+ gramSchmidt_inv_triangular
+ gramSchmidt_linearIndependent
+ gramSchmidt_mem_span
+ gramSchmidt_ne_zero
+ gramSchmidt_ne_zero_coe
+ gramSchmidt_of_orthogonal
+ gramSchmidt_orthogonal
+ gramSchmidt_pairwise_orthogonal
+ gramSchmidt_zero
+ hloc_TODO
+ hoge
+ injective_mfderiv_of_eventually_leftInverse
+ injective_symm
+ instance (cov : CovariantDerivative I F V) {s : Set M} :
+ instance (f : F) : CoeOut (TangentSpace 𝓘(ℝ, F) f) F
+ instance (x : B) : AddCommGroup (W E x) := by
+ instance (x : B) : ContinuousAdd (V E x) := by
+ instance (x : B) : ContinuousSMul ℝ (V E x) := by
+ instance (x : B) : IsTopologicalAddGroup (V E x) := by
+ instance (x : B) : Module ℝ (V E x) := by
+ instance (x : B) : Module ℝ (W E x) := by
+ instance (x : B) : TopologicalSpace (W E x) := by
+ instance : (x : B) → AddCommGroup (V E x) := by
+ instance : (x : B) → TopologicalSpace (V E x) := by
+ instance : CoeFun (CovariantDerivative I F V)
+ instance : ContMDiffVectorBundle n (F →L[ℝ] F →L[ℝ] ℝ) (W E) IB := by
+ instance : ContMDiffVectorBundle n (F →L[ℝ] ℝ) (V E) IB := by
+ instance : FiberBundle (F →L[ℝ] F →L[ℝ] ℝ) (W E) := by
+ instance : FiberBundle (F →L[ℝ] ℝ) (V E) := by
+ instance : TopologicalSpace (TotalSpace (F →L[ℝ] F →L[ℝ] ℝ) (W E)) := by
+ instance : TopologicalSpace (TotalSpace (F →L[ℝ] ℝ) (V E)) := by
+ instance : VectorBundle ℝ (F →L[ℝ] F →L[ℝ] ℝ) (W E) := by
+ instance : VectorBundle ℝ (F →L[ℝ] ℝ) (V E) := by
+ invFun_comp_eventuallyEq
+ isBilinearMap_differenceAux
+ isBilinearMap_eval
+ isBilinearMap_evalL
+ isCovariantDerivativeOn_lcCandidate
+ isCovariantDerivativeOn_lcCandidateAux
+ isCovariantDerivativeOn_lcCandidateAux_of_nonempty
+ isCovariantDerivativeOn_pushCovDer
+ isTorsionFreeOn_iff_christoffelSymbols
+ isTorsionFreeOn_univ
+ isTorsionFree_def
+ isTorsionFree_iff
+ isTorsionFree_iff_christoffelSymbols'
+ is_good_localSection
+ isolate_aux
+ lcCandidate
+ lcCandidateAux
+ lcCandidate_eq_lcCandidateAux
+ leviCivitaRhs
+ leviCivitaRhs'
+ leviCivitaRhs'_addX
+ leviCivitaRhs'_addX_apply
+ leviCivitaRhs'_addY_apply
+ leviCivitaRhs'_addZ
+ leviCivitaRhs'_addZ_apply
+ leviCivitaRhs'_smulX_apply
+ leviCivitaRhs'_smulY_apply
+ leviCivitaRhs'_smulY_const_apply
+ leviCivitaRhs'_smulZ
+ leviCivitaRhs'_smulZ_apply
+ leviCivitaRhs_addX
+ leviCivitaRhs_addX_apply
+ leviCivitaRhs_addY
+ leviCivitaRhs_addY_apply
+ leviCivitaRhs_addZ
+ leviCivitaRhs_addZ_apply
+ leviCivitaRhs_apply
+ leviCivitaRhs_smulX
+ leviCivitaRhs_smulX_apply
+ leviCivitaRhs_smulY_apply
+ leviCivitaRhs_smulY_const
+ leviCivitaRhs_smulY_const_apply
+ leviCivitaRhs_smulZ
+ localExtensionOn
+ localExtensionOn_apply_self
+ localExtensionOn_localFrame_coeff
+ local_section_at
+ map_add
+ map_of
+ map_of_loc_one_jet
+ map_of_loc_one_jet_spec
+ map_of_one_jet
+ map_of_one_jet_spec
+ map_of_spec
+ map_smul
+ mdifferentiableAt
+ mdifferentiableAt_dependent_congr
+ mdifferentiableAt_invFun
+ mdifferentiableAt_section_of_function
+ mdifferentiable_dependent_congr_iff
+ mdifferentiable_extend
+ mem_horiz_iff_exists
+ mem_horiz_iff_proj
+ mem_span_gramSchmidt
+ mfderiv_comp_section
+ mfderiv_const_smul
+ mfderiv_proj_derivInv_apply
+ mfderiv_proj_fst_deriv
+ mfderiv_smul
+ mlieBracketWithin_smul_left
+ mlieBracketWithin_smul_right
+ mlieBracket_smul_left
+ mlieBracket_smul_right
+ mpullbackWithin_const_smul
+ mpullbackWithin_const_smul_apply
+ mpullback_const_smul
+ mpullback_const_smul_apply
+ mynorm
+ of_isCovariantDerivativeOn_of_open_cover
+ of_isCovariantDerivativeOn_of_open_cover_coe
+ of_isTorsionFreeOn_of_open_cover
+ of_subsingleton
+ one_form
+ orthonormalFrame
+ orthonormalFrame_apply_of_notMem
+ orthonormalFrame_isOrthonormalFrameOn
+ preimage_baseSet_mem_nhds
+ product
+ product_add_left
+ product_add_left_apply
+ product_add_right
+ product_add_right_apply
+ product_apply
+ product_congr_left
+ product_congr_left₂
+ product_congr_right
+ product_congr_right₂
+ product_neg_left
+ product_neg_right
+ product_smul_const_left
+ product_smul_const_right
+ product_smul_left
+ product_smul_right
+ product_sub_left
+ product_sub_right
+ product_swap
+ product_zero_left
+ product_zero_right
+ proj
+ proj_acceleration
+ proj_invFun_eventuallyEq
+ proj_mderiv
+ proj_velocity
+ projection
+ projection_apply
+ pushCovDer
+ pushCovDer_isCovariantDerivativeOn
+ pushCovDer_ofSect
+ qux
+ rhs_aux
+ rhs_aux_addX
+ rhs_aux_addY
+ rhs_aux_addY_apply
+ rhs_aux_addZ
+ rhs_aux_addZ_apply
+ rhs_aux_smulX
+ rhs_aux_smulX_apply
+ rhs_aux_smulY
+ rhs_aux_smulY_apply
+ rhs_aux_smulY_const
+ rhs_aux_smulY_const_apply
+ rhs_aux_smulZ
+ rhs_aux_smulZ_apply
+ rhs_aux_smulZ_const
+ rhs_aux_smulZ_const_apply
+ rhs_aux_swap
+ smul_const_X
+ snd_triv_proj
+ span_gramSchmidt
+ span_gramSchmidtNormed
+ span_gramSchmidtNormed_range
+ span_gramSchmidt_Iic
+ span_gramSchmidt_Iio
+ surjective_mfderiv_of_eventually_rightInverse
+ surjective_symm
+ symm_apply_apply_mk_eventuallyEq
+ symm_map_add
+ symm_map_smul
+ symm_map_zero
+ tensoriality_criterion
+ tensoriality_criterion'
+ tensoriality_criterion''
+ tensoriality_criterion₂
+ tensoriality_criterion₂'
+ torsion_add_left
+ torsion_add_left_apply
+ torsion_add_right
+ torsion_add_right_apply
+ torsion_antisymm
+ torsion_self
+ torsion_smul_left
+ torsion_smul_left_apply
+ torsion_smul_right
+ torsion_smul_right_apply
+ torsion_tensorial
+ torsion_zero
+ torsion_zero'
+ trivial_isSmooth
+ velocity
++ affineCombination
++ affineCombination'
++ aux
++ congr
++ horiz
++ horiz_vert_direct_sum
++ iUnion
++ mono
++ of_endomorphism
++ sum_X
++ trivial
++ zeroX
++ zeroσ

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (3.41, 0.03)

Current number	Change	Type
140	2	flexible linter exceptions
638	9	erw
10066	17	backward.isDefEq

Current commit c487a9a1d2
Reference commit 7c0aa26a8b

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: add lemma mdifferentiableAt_totalSpace #26360
• [Merged by Bors] - feat: add continuousOn_iUnion #26672
• [Merged by Bors] - feat: contMDiffOn_iUnion_iff_of_isOpen #26673
• [Merged by Bors] - feat: finite sum, difference, scalar product of C^k sections is C^k #26674
• [Merged by Bors] - chore(VectorBundle/Basic): minor clean-ups and polish #26864
• [Merged by Bors] - feat(VectorBundle/MDifferentiable): add some basic API #26865
• [Merged by Bors] - feat(VectorBundle/MDifferentiable): differentiability results for coordChange #26866
• [Merged by Bors] - feat: mdifferentiableOn_section_of_mem_baseSet₀ #26870
• [Merged by Bors] - feat: finite sum, difference, scalar product of differentiable sections is differentiable #26871
• [Merged by Bors] - feat: contMDiff_section_of_tsupport #26671
• [Merged by Bors] - feat: contMDiffWithinAt_zeroSection #26676
• [Merged by Bors] - chore(Geometry/Manifold/VectorBundle/Basic): make some arguments implicit #26677
• [Merged by Bors] - feat: contMDiffOn_section_of_mem_baseSet #26678
• [Merged by Bors] - feat: DifferentiableOn.iUnion #26686
• [Merged by Bors] - feat: MDifferentiableOn.iUnion #26687
• [Merged by Bors] - feat: ContDiffOn.iUnion #26688
• [Merged by Bors] - feat: add missing API for MDifferentiable*.{add,neg} #26702
• [Merged by Bors] - feat: missing congruence lemmas for mdifferentiability #26709
• [Merged by Bors] - feat: Lie bracket with zero is zero #26734
• [Merged by Bors] - feat: product rule for Lie bracket on manifolds #26743
• [Merged by Bors] - chore(Gram-Schmidt): small tweaks #26894
• [Merged by Bors] - feat: add mdifferentiable analogues of C^n metric lemmas #26921
• [Merged by Bors] - feat: add mdifferentiable version of hom bundle smoothness lemmas #26922
• feat: Finite.linearOrder, choosing *some* linear order on a finite type #27020
• [Merged by Bors] - feat: custom elaborators for differential geometry #27021
• [Merged by Bors] - feat: support coercions in the differential geometry elaborators #30307
• [Merged by Bors] - feat: gramSchmidtNormed_linearIndependent and minor tweaks #27023
• feat: Gram-Schmidt orthonormalisation for sections of a vector bundle #27024
• feat: Gram-Schmidt procedure on smooth vector bundles yields smooth sections #27025
• [Merged by Bors] - feat: local frames in a vector bundle #30338
• [Merged by Bors] - feat: local frames in a vector bundle #30083
• feat: extend a tangent vector for a locally smooth vector field #30339
• [Merged by Bors] - feat: add #check' command and tactic, which only show explicit arguments #31194
• feat: add mfderiv_const_smul #34262
• [Merged by Bors] - feat: mfderiv_smul #34263
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[grunweg]

For the record: #36036 builds on this branch, completely refactoring covariant derivatives. Probably, this branch should be closed in favour of that one (at some point).