Zulip Chat Archive
Stream: mathlib4
Topic: NonZeroDivisorLeft and NonZeroDivisor
Andrew Yang (Dec 05 2023 at 18:07):
docs#nonZeroDivisorsLeft is definitionally equal to docs#nonZeroDivisors. Should we get rid of one of them or change the definition of nonZeroDivisors
to the intersection of nonZeroDivisorsLeft
and nonZeroDivisorsRight
?
Last updated: Dec 20 2023 at 11:08 UTC