Commit 2025-04-28 16:25 f74ebecf

View on Github →

chore(Algebra/Module/PID): fix universe level (#24403) Originally the structure theorem of finitely generated torsion modules N over PID R : Type u required that N : Type max u v. This PR fixes it to M : Type v. Now that lequivProdOfRightSplitExact is universe polymorphic, we can also drop the use of ULift.moduleEquiv in the proofs.

Estimated changes

Modified Mathlib/Algebra/Module/PID.lean

modified theorem Module.equiv_directSum_of_isTorsion

modified theorem Module.equiv_free_prod_directSum

modified theorem Module.torsion_by_prime_power_decomposition