is_non_zero_divisor

Stream: new members

[Damiano Testa]

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]

These are sometimes called regular elements, right?

[Johan Commelin]

Should we distinguish left_regular and right_regular?

[Damiano Testa]

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!