max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Grind/Ordered
History
Leonardo de Moura 9ece4e463a
refactor: NoNatZeroDivisors (#8909) 
This PR refactors the `NoNatZeroDivisors` to make sure it will work with
the new `Semiring` support.
2025-06-21 03:01:05 +00:00
..
Field.lean feat: generalize grind IsCharP instance (#8848) 2025-06-18 02:49:26 +00:00
Int.lean chore: move grind algebra instances into Init.GrindInstances (#8830) 2025-06-17 03:59:15 +00:00
Linarith.lean refactor: NoNatZeroDivisors (#8909) 2025-06-21 03:01:05 +00:00
Module.lean feat: add doc-string to grind algebra typeclasses (#8890) 2025-06-20 04:05:47 +00:00
Order.lean feat: add doc-string to grind algebra typeclasses (#8890) 2025-06-20 04:05:47 +00:00
Ring.lean feat: add doc-string to grind algebra typeclasses (#8890) 2025-06-20 04:05:47 +00:00