Commit 2021-04-28 19:37 abf1c205
View on Github →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.