finite_free wishlist

Stream: condensed mathematics

[Riccardo Brasca]

Following Johan's suggestion, I will work to build an API for finite_free modules, extending what Kevin has done for finite_free groups.
Besides obvious things like finite_free implies finite, do we need any particular result?

[Riccardo Brasca]

I am thinking especially about direct sum, that are easy mathematically, but I don't the status of this in mathlib.

[Johan Commelin]

@Riccardo Brasca I would suggest that we drop finite_free, and just have module.finite and module.free

[Kevin Buzzard]

I am happy with this, I just wrote down finite_free because I needed it, I didn't put too much thought into it. Probably module.finite and module.free is a much better approach.