feat(Algebra/Module): snake lemma

[erdOne]

---

[github-actions]

PR summary 5f7372ae57

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Module.SnakeLemma	873

---

Declarations diff

+ SnakeLemma.eq_of_eq
+ SnakeLemma.exact_δ'_left
+ SnakeLemma.exact_δ'_right
+ SnakeLemma.exact_δ_left
+ SnakeLemma.exact_δ_right
+ SnakeLemma.δ
+ SnakeLemma.δ'
+ SnakeLemma.δ'_eq
+ SnakeLemma.δ_aux
+ SnakeLemma.δ_eq

You can run this locally as follows

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

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

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

[joelriou]

Suggested change

	Such that `f₂` is surjective with a (set-theoretic) section `ρ`, `g₁` is injective with a
	(set-theoretic) retraction `π`,
	then the map `π₁ ∘ ρ ∘ i₂ ∘ σ ∘ ι₃` is a linear map from `K₃` to `C₁`.
	Such that `f₂` is surjective with a (set-theoretic) section `σ`, `g₁` is injective with a
	(set-theoretic) retraction `ρ`,
	then the map `π₁ ∘ ρ ∘ i₂ ∘ σ ∘ ι₃` is a linear map from `K₃` to `C₁`.

[joelriou]

The same typo appears in several other places in the file.