Theorem Submodule.exists_isInternal_prime_power_torsion

Modification history

2023-06-05 20:26
Mathlib/Algebra/Module/DedekindDomain.lean
feat: port Algebra.Module.DedekindDomain (#4705)
Added Submodule.exists_isInternal_prime_power_torsionView on Github →