basic): remove dependency on finiteness (#17764)

Commit

3 years ago

chore(algebra/module/basic): remove dependency on finiteness (#17764) Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Author

hrmacbeth

Parents

7080d596

mathlib 94825b2b - chore(algebra/module/basic): remove dependency on finiteness (#17764)

mathlib
94825b2b - chore(algebra/module/basic): remove dependency on finiteness (#17764)