feat(linear_algebra/free_module): add class module.free (#7801)
feat(linear_algebra/free_module): add class module.free (#7801)

We introduce here a new class `module.free`.



Co-authored-by: Johan Commelin <759412786bc533369b22377bf83fb9056c5b25b2@commelin.net>

leanprover-community/mathlib,leanprover-community/mathlib