Commit 2023-06-05 20:26 47535ddd

View on Github →

feat: port Algebra.Module.DedekindDomain (#4705)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/DedekindDomain.lean

added theorem Submodule.exists_isInternal_prime_power_torsion

added theorem Submodule.isInternal_prime_power_torsion

added theorem Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal