Commit 2025-08-11 11:23 0a75191a

View on Github →

feat(Algebra): connect IsRegular/IsCancelMul to nonZeroDivisors/NoZeroDivisors (#27877)

Show that a regular element is not a zero divisors, and the converse holds in a ring.
Show that Is(Left/Right)CancelMul and NoZeroDivisors are equivalent for a ring.

Estimated changes

Modified Mathlib/Algebra/Divisibility/Basic.lean

added theorem IsLeftRegular.dvd_cancel_left

Modified Mathlib/Algebra/GroupWithZero/Defs.lean

added theorem noZeroDivisors_iff_eq_zero_of_mul

added theorem noZeroDivisors_iff_left_eq_zero_of_mul

added theorem noZeroDivisors_iff_right_eq_zero_of_mul

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

added theorem IsLeftRegular.mem_nonZeroDivisorsLeft

added theorem IsRegular.mem_nonZeroDivisors

added theorem IsRightRegular.mem_nonZeroDivisorsRight

added theorem IsSMulRegular.mem_nonZeroSMulDivisors

added theorem isSMulRegular_iff_mem_nonZeroSMulDivisors

added theorem noZeroDivisors_iff_forall_mem_nonZeroDivisors

added theorem noZeroDivisors_iff_forall_mem_nonZeroDivisorsLeft

added theorem noZeroDivisors_iff_forall_mem_nonZeroDivisorsRight

added theorem noZeroSMulDivisors_iff_forall_mem_nonZeroSMulDivisors

modified def nonZeroDivisors

Modified Mathlib/Algebra/NoZeroSMulDivisors/Defs.lean

added theorem noZeroSMulDivisors_iff_right_eq_zero_of_smul

Modified Mathlib/Algebra/Regular/Prod.lean

Modified Mathlib/Algebra/Regular/SMul.lean

deleted theorem IsSMulRegular.eq_zero_of_smul_eq_zero

deleted theorem IsSMulRegular.of_injective

added theorem isSMulRegular_iff_right_eq_zero_of_smul

Modified Mathlib/Algebra/Ring/Basic.lean

modified theorem isCancelMulZero_iff_noZeroDivisors

added theorem isLeftRegular_iff_right_eq_zero_of_mul

added theorem isRegular_iff_eq_zero_of_mul

added theorem isRightRegular_iff_left_eq_zero_of_mul

added theorem noZeroDivisors_tfae

Modified Mathlib/Algebra/Ring/NonZeroDivisors.lean

deleted theorem IsLeftRegular.mem_nonZeroDivisorsLeft

deleted theorem IsRightRegular.mem_nonZeroDivisorsRight

modified theorem dvd_cancel_right_mem_nonZeroDivisors

modified theorem isRegular_iff_mem_nonZeroDivisors

modified theorem mul_cancel_left_mem_nonZeroDivisors

Modified Mathlib/Data/Finsupp/SMul.lean

Modified Mathlib/Data/Matrix/Diagonal.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

added theorem IsSMulRegular.of_injective

Modified Mathlib/RingTheory/Regular/IsSMulRegular.lean

deleted theorem isSMulRegular_iff_mem_nonZeroSMulDivisors

deleted theorem isSMulRegular_iff_smul_eq_zero_imp_eq_zero

deleted theorem isSMulRegular_of_smul_eq_zero_imp_eq_zero

deleted theorem isSMulRegular_on_quot_iff_smul_mem_implies_mem

deleted theorem isSMulRegular_on_submodule_iff_mem_imp_smul_eq_zero_imp_eq_zero

added theorem isSMulRegular_quotient_iff_mem_of_smul_mem

added theorem isSMulRegular_submodule_iff_right_eq_zero_of_smul

deleted theorem mem_of_isSMulRegular_on_quot_of_smul_mem

added theorem mem_of_isSMulRegular_quotient_of_smul_mem