feat(linear_algebra): free_of_finite_type_torsion_free (#7341)
A finite type torsion free module over a PID is free.
There are also some tiny preliminaries, and I moved `submodule.map_span` to `linear_map.map_span` to allow using the dot notation more often.
