torsion.lean): various lemmas about torsion modules (#14573)

Commit

3 years ago

feat(algebra/module/torsion.lean): various lemmas about torsion modules (#14573) An intermediate PR for various lemmas about torsion modules needed at #13524

Author

pbazin

Parents

dfc54a3a

mathlib3 c2bb59e5 - feat(algebra/module/torsion.lean): various lemmas about torsion modules (#14573)

mathlib3
c2bb59e5 - feat(algebra/module/torsion.lean): various lemmas about torsion modules (#14573)