division_ring'

Stream: maths

[Johan Commelin]

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]

or we move to Lean fork and change the definition of division ring...

[Kenny Lau]

or we wait for Lean 4

[Yury G. Kudryashov]

Is there any information about the planned changes to algebraic classes structure in Lean 4?