Theorem Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal

Modification history

2026-02-27 09:51
Mathlib/Algebra/Module/DedekindDomain.lean
feat: classical "decidability" instances on sets and ideals (#33757) …
Modified Submodule.isInternal_prime_power_torsion_of_is_torsion_by_idealView on Github →
2024-08-03 10:01
Mathlib/Algebra/Module/DedekindDomain.lean
chore: remove some uses of `open Classical`, part 2 (#15413) …
Modified Submodule.isInternal_prime_power_torsion_of_is_torsion_by_idealView on Github →
2023-06-05 20:26
Mathlib/Algebra/Module/DedekindDomain.lean
feat: port Algebra.Module.DedekindDomain (#4705)
Added Submodule.isInternal_prime_power_torsion_of_is_torsion_by_idealView on Github →