## Stream: new members

### Topic: zero divisors

#### 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))


Congrats!

#### Kevin Buzzard (May 17 2020 at 08:33):

Do we have zero divisors in mathlib?

#### Yury G. Kudryashov (May 17 2020 at 08:47):

We have non_zero_divisors

#### Yury G. Kudryashov (May 17 2020 at 08:47):

In ring/localization.

Last updated: May 13 2021 at 23:16 UTC