Zulip Chat Archive

Stream: new members

Topic: is_non_zero_divisor

Damiano Testa (Feb 17 2021 at 14:03):

Dear All,

motivated by https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews, here is a proposal at a definition of non_zero_divisors. Any comments are more than welcome!

def is_non_zero_divisor {R : Type*} [semiring R] (c : R) : Prop :=
( a b : R, a * c = b * c  a = b)  ( a b : R, c * a = c * b  a = b)

Johan Commelin (Feb 17 2021 at 14:07):

These are sometimes called regular elements, right?

Johan Commelin (Feb 17 2021 at 14:07):

Should we distinguish left_regular and right_regular?

Damiano Testa (Feb 17 2021 at 14:09):

I am happy to distinguish left and right, although I do not have a specific non-commutative application in mind.

Calling these elements regular works well for me! After all, I would like to see regular_sequences!

Last updated: Dec 20 2023 at 11:08 UTC