Commit 2024-02-05 02:27 c174b2de

View on Github →

chore(Module/Torsion): drop DecidableEq assumptions (#10253)

Estimated changes

Modified Mathlib/Algebra/Module/Torsion.lean

modified theorem Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf

modified theorem Submodule.iSup_torsionBy_eq_torsionBy_prod

modified theorem Submodule.supIndep_torsionBy

modified theorem Submodule.supIndep_torsionBySet_ideal