Update Mathlib/LinearAlgebra/Basis/Exact.lean

Co-authored-by: Andrew Yang <[email protected]>

Mathlib/LinearAlgebra/Basis/Exact.lean

@@ -10,7 +10,7 @@ import Mathlib.LinearAlgebra.Basis.Basic
 /-!
 # Basis from a split exact sequence
 
-Let `0 → K → M → P → 0` be an exact sequence of `R`-modules, let `s : M → K` be a
+Let `0 → K → M → P → 0` be a split exact sequence of `R`-modules, let `s : M → K` be a
 retraction of `f` and `v` be a basis of `M` indexed by `κ ⊕ σ`. Then
 if `s vᵢ = 0` for `i : κ` and `(s vⱼ)ⱼ` is linear independent for `j : σ`, then
 the images of `vᵢ` for `i : κ` form a basis of `P`.