mathlib

abf1c205 - feat(linear_algebra/free_module): free of finite torsion free (#7381)

feat(linear_algebra/free_module): free of finite torsion free (#7381) This is a reformulation of module.free_of_finite_type_torsion_free in terms of `ring_theory.finiteness` (combining my recent algebra PRs). Note this adds an import but it seems ok to me.