Commit 2023-07-05 15:33 b72d935a

View on Github →

feat: port Algebra.Module.PID (#4707)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Module/PID.lean

added theorem Ideal.torsionOf_eq_span_pow_pOrder

added theorem Module.equiv_directSum_of_isTorsion

added theorem Module.equiv_free_prod_directSum

added theorem Module.exists_smul_eq_zero_and_mk_eq

added theorem Module.p_pow_smul_lift

added theorem Module.torsion_by_prime_power_decomposition

added theorem Submodule.exists_isInternal_prime_power_torsion_of_pid

added theorem Submodule.isInternal_prime_power_torsion_of_pid