Zulip Chat Archive

Stream: new members

Topic: zero divisors


view this post on Zulip Aniruddh Agarwal (May 17 2020 at 04:18):

I just managed to define zero divisors and prove that 0 is a zero divisor in a nonzero ring!

def is_zero_divisor (a : R) :=  b : R, b  0  a * b = 0

theorem zero_is_zero_divisor_in_nonzero_ring [nonzero_comm_ring α] : is_zero_divisor (0 : α) :=
  exists.intro (1 : α) (and.intro (one_ne_zero) (by simp))

view this post on Zulip Kenny Lau (May 17 2020 at 08:31):

Congrats!

view this post on Zulip Kevin Buzzard (May 17 2020 at 08:33):

Do we have zero divisors in mathlib?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 08:47):

We have non_zero_divisors

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 08:47):

In ring/localization.


Last updated: May 13 2021 at 23:16 UTC