A surjection of finite free modules splits
Rank is additive on short exact sequences
Let \(R\) be a noetherian ring. Then \(R[x]\) is noetherian.
The proof of this is already in mathlib: