Commit 2024-11-28 16:12 0be336ff
View on Github →feat: MulLeftMono implies PosMulMono (#19248)
... and similarly for the other typeclasses
From GrowthInGroups (LeanCamCombi)
feat: MulLeftMono implies PosMulMono (#19248)
... and similarly for the other typeclasses
From GrowthInGroups (LeanCamCombi)