Zulip Chat Archive

Stream: maths

Topic: division_ring'


view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Dec 04 2019 at 16:47):

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

view this post on Zulip Kenny Lau (Dec 04 2019 at 16:49):

or we wait for Lean 4

view this post on Zulip 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