This file proves that a finite stably free module M is free if it is invertible.

theorem Module.free_of_isStablyFree_of_invertible (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsStablyFree R M] [Module.Invertible R M] : Free R M

Let R be a commutative ring, M be a finite stably free R-module. Then M is free if it is invertible.