mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: MulPosMono (WithZero α)

Open kbuzzard opened this issue 1 year ago • 1 comments
trafficstars

These instances make it possible to argue with multiplication and inequalities in ℤₘ₀ .

Open in Gitpod

These instances are in a bit of a funny place (they need MulPosMono and WithZero) -- any ideas about a better place to put them are welcome.

kbuzzard avatar May 22 '24 08:05 kbuzzard

Could you move that to the folder Algebra.Order.GroupWithZero? Maybe in the file Algebra.Order.GroupWithZero.WithZero?

YaelDillies avatar May 22 '24 19:05 YaelDillies

Thanks!

bors d+

riccardobrasca avatar May 23 '24 13:05 riccardobrasca

:v: kbuzzard can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mathlib-bors[bot] avatar May 23 '24 13:05 mathlib-bors[bot]

Thanks all!

bors r+

kbuzzard avatar May 23 '24 14:05 kbuzzard

Pull request successfully merged into master.

Build succeeded:

mathlib-bors[bot] avatar May 23 '24 14:05 mathlib-bors[bot]