Johan Commelin (Dec 04 2019 at 09:27):
Should we port all division_ring stuff to
division_ring' that fixes
0¯¹ = 0? Because now we end up proving lots of stuff for fields because division_ring is too annoying to work with.
Floris van Doorn (Dec 04 2019 at 16:47):
or we move to Lean fork and change the definition of division ring...
Kenny Lau (Dec 04 2019 at 16:49):
or we wait for Lean 4
Yury G. Kudryashov (Dec 04 2019 at 18:04):
Is there any information about the planned changes to algebraic classes structure in Lean 4?
Last updated: May 14 2021 at 18:28 UTC