Zulip Chat Archive

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

Kenny Lau (May 17 2020 at 08:31):

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: Dec 20 2023 at 11:08 UTC