Commit 2023-03-13 14:02 e3554190

View on Github →

feat: Port/LinearAlgebra.Smodeq (#2788) Depends on synthInstance.etaExperiment or permanent replacement.

Estimated changes

added theorem SModEq.add
added theorem SModEq.bot
added theorem SModEq.comap
added theorem SModEq.eval
added theorem SModEq.map
added theorem SModEq.mono
added theorem SModEq.smul
added theorem SModEq.sub_mem
added theorem SModEq.top
added theorem SModEq.zero
added def SModEq