Zulip Chat Archive

Stream: general

Topic: field'

Kenny Lau (Feb 23 2019 at 10:32):

set_option old_structure_cmd true
class field' (α : Type u) extends division_ring α, comm_ring α :=
(inv_zero : (0:α)⁻¹ = 0)

Kenny Lau (Feb 23 2019 at 10:32):

Does this have a place in mathlib?

Last updated: May 02 2025 at 03:31 UTC