Finite and projective modules

theorem Module.Finite.exists_comp_eq_id_of_projective (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Projective R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M) (g : M →ₗ[R] Fin n → R), Function.Surjective ⇑f ∧ Function.Injective ⇑g ∧ f ∘ₗ g = LinearMap.id