feat(algebra/regular): define regular elements (#6282)
feat(algebra/regular): define regular elements (#6282)

The goal of this PR is to start the API for regular elements.  The final goal is to talk about non-zero-divisors.

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/is_regular





leanprover-community/mathlib,leanprover-community/mathlib