Def Module.DirectLimit.moduleCon

Modification history

2025-10-31 11:48

Mathlib/Algebra/Colimit/Module.lean

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

Added Module.DirectLimit.moduleCon View on Github →