Commit 2025-10-31 11:48 72c18d78

View on Github →

feat(Algebra): congruence relation respecting SMul (#30665)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Colimit/Module.lean

added def Module.DirectLimit.moduleCon

modified def Module.DirectLimit

Created Mathlib/Algebra/Module/Congruence/Defs.lean

added def ModuleCon.ker

added structure ModuleCon

added def SMulCon.addConGen'

added def SMulCon.ker

added structure SMulCon

added structure VAddCon

Modified Mathlib/GroupTheory/Congruence/Defs.lean

Modified Mathlib/RingTheory/Finiteness/Cardinality.lean

Modified Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean

modified theorem Module.freeLocus_eq_univ