feat: the Levi-Civita connection on a manifold

[grunweg]

---

• depends on: feat: metric connections #36299

[github-actions]

PR summary 424dce2f30

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric (new file)	2209
Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita (new file)	2294

---

Declarations diff

+ IsCompatible
+ IsLeviCivitaConnection
+ IsLeviCivitaConnection.eq_leviCivitaRhs
+ IsLeviCivitaConnection.uniqueness
+ LeviCivitaConnection
+ _root_.MDifferentiable.inner_bundle'
+ _root_.MDifferentiableAt.inner_bundle'
+ aux
+ compatibilityTensor
+ compatibilityTensorAux
+ compatibilityTensorAux_apply
+ compatibilityTensorAux_tensorial₁
+ compatibilityTensorAux_tensorial₂
+ compatibilityTensor_apply
+ compatibilityTensor_apply_eq_extend
+ congr_of_forall_product
+ congr_of_forall_product_apply
+ fromTangentSpace_mfderiv_add
+ fromTangentSpace_mfderiv_add_apply
+ isCompatible_iff
+ isCovariantDerivativeOn_lcAux
+ lcAux
+ lcAux_apply
+ lcAux₀
+ lcAux₀'
+ lcAux₀_apply
+ lcAux₁
+ lcAux₁_apply
+ leviCivitaConnection_apply
+ leviCivitaConnection_isCompatible
+ leviCivitaConnection_isCompatible_aux
+ leviCivitaConnection_isLeviCivitaConnection
+ leviCivitaConnection_torsion_eq_zero
+ 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
+ leviCivitaRhs_smulZ_apply
+ leviCivitaRhs_tensorial₁
+ leviCivitaRhs_tensorial₂
+ 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
+ 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

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: metric connections #36299
  By Dependent Issues (🤖). Happy coding!