Theorem Module.finite_finsupp_iff

feat: `ι →₀ R` is a finite `R`-module iff `ι` is finite (#23997)