basis from basis of subspace and quotient

Stream: Is there code for X?

[Antoine Chambert-Loir]

If V is an R-module and W is a free submodule such that V/W is free, then V is free. More precisely, one can get a basis of V by combining a basis of W with the lift of a basis of V/W. Is this in mathlib already?

[Junyan Xu]

docs#LinearIndependent.sumElim_of_quotient is basically one half of it, a But maybe it's easier to use docs#lequivProdOfLeftSplitExact mentioned at #Is there code for X? > Structure of `(ZMod n)ˣ` @ 💬

[Antoine Chambert-Loir]

#32560

[Antoine Chambert-Loir]

I used the first method. (The goal was the determinant equality which is also proved there.)