Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-20 17:42 ee8708e4

View on Github →

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

Estimated changes

Created src/algebra/regular.lean

added theorem is_left_regular.mul

added theorem is_left_regular.of_mul

added theorem is_left_regular.subsingleton

added def is_left_regular

added theorem is_left_regular_of_left_cancel_semigroup

added theorem is_left_regular_of_mul_eq_one

added theorem is_left_regular_zero_iff_subsingleton

added theorem is_regular.and_of_mul_of_mul

added theorem is_regular.subsingleton

added structure is_regular

added theorem is_regular_iff_subsingleton

added theorem is_regular_mul_and_mul_iff

added theorem is_regular_mul_iff

added theorem is_regular_of_cancel_monoid

added theorem is_regular_of_cancel_monoid_with_zero

added theorem is_regular_one

added theorem is_right_regular.mul

added theorem is_right_regular.of_mul

added theorem is_right_regular.subsingleton

added def is_right_regular

added theorem is_right_regular_of_mul_eq_one

added theorem is_right_regular_of_right_cancel_semigroup

added theorem is_right_regular_zero_iff_subsingleton

added theorem is_unit.is_regular

added theorem mul_is_left_regular_iff

added theorem mul_is_right_regular_iff

added theorem not_is_left_regular_zero_iff

added theorem not_is_right_regular_zero_iff

added theorem units.is_regular