Commit 2025-10-30 18:05 22765e8d

View on Github →

chore: move SModEq to a new folder (#30990) Split off from #30989. I only move it to a new folder and do nothing else.

Estimated changes

deleted theorem SModEq.add
deleted theorem SModEq.bot
deleted theorem SModEq.comap
deleted theorem SModEq.comm
deleted theorem SModEq.eval
deleted theorem SModEq.map
deleted theorem SModEq.mono
deleted theorem SModEq.mul
deleted theorem SModEq.neg
deleted theorem SModEq.nsmul
deleted theorem SModEq.pow
deleted theorem SModEq.prod
deleted theorem SModEq.smul
deleted theorem SModEq.sub
deleted theorem SModEq.sub_mem
deleted theorem SModEq.sum
deleted theorem SModEq.top
deleted theorem SModEq.zero
deleted theorem SModEq.zsmul
deleted def SModEq
deleted theorem sub_smodEq_zero
added theorem SModEq.add
added theorem SModEq.bot
added theorem SModEq.comap
added theorem SModEq.comm
added theorem SModEq.eval
added theorem SModEq.map
added theorem SModEq.mono
added theorem SModEq.mul
added theorem SModEq.neg
added theorem SModEq.nsmul
added theorem SModEq.pow
added theorem SModEq.prod
added theorem SModEq.smul
added theorem SModEq.sub
added theorem SModEq.sub_mem
added theorem SModEq.sum
added theorem SModEq.top
added theorem SModEq.zero
added theorem SModEq.zsmul
added def SModEq
added theorem sub_smodEq_zero