Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-09 08:02 8fb5c46f

View on Github →

chore(algebra/ring/basic): move results about regular elements (#16865)

Estimated changes

Modified src/algebra/ring/basic.lean

deleted theorem is_left_regular_of_non_zero_divisor

deleted theorem is_regular_iff_ne_zero'

deleted theorem is_regular_of_ne_zero'

deleted theorem is_right_regular_of_non_zero_divisor

deleted def no_zero_divisors.to_cancel_comm_monoid_with_zero

deleted def no_zero_divisors.to_cancel_monoid_with_zero

Created src/algebra/ring/regular.lean

added theorem is_left_regular_of_non_zero_divisor

added theorem is_regular_iff_ne_zero'

added theorem is_regular_of_ne_zero'

added theorem is_right_regular_of_non_zero_divisor

added def no_zero_divisors.to_cancel_comm_monoid_with_zero

added def no_zero_divisors.to_cancel_monoid_with_zero

Modified src/data/int/basic.lean

Modified src/data/set/intervals/instances.lean