Commit 2023-01-20 18:12 5d81ca10

View on Github →

feat: port RingTheory.NonZeroDivisors (#1717)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/NonZeroDivisors.lean

added theorem eq_zero_of_ne_zero_of_mul_left_eq_zero

added theorem eq_zero_of_ne_zero_of_mul_right_eq_zero

added theorem isUnit_of_mem_nonZeroDivisors

added theorem le_nonZeroDivisors_of_noZeroDivisors

added theorem map_le_nonZeroDivisors_of_injective

added theorem map_mem_nonZeroDivisors

added theorem map_ne_zero_of_mem_nonZeroDivisors

added theorem mem_nonZeroDivisors_iff

added theorem mem_nonZeroDivisors_iff_ne_zero

added theorem mem_nonZeroDivisors_of_ne_zero

added theorem mul_cancel_left_coe_non_zero_divisor

added theorem mul_cancel_left_mem_non_zero_divisor

added theorem mul_cancel_right_coe_non_zero_divisor

added theorem mul_cancel_right_mem_non_zero_divisor

added theorem mul_left_coe_nonZeroDivisors_eq_zero_iff

added theorem mul_left_mem_nonZeroDivisors_eq_zero_iff

added theorem mul_mem_nonZeroDivisors

added theorem mul_right_coe_nonZeroDivisors_eq_zero_iff

added theorem mul_right_mem_nonZeroDivisors_eq_zero_iff

added theorem nonZeroDivisors.coe_ne_zero

added theorem nonZeroDivisors.ne_zero

added def nonZeroDivisors

added theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective

added theorem powers_le_nonZeroDivisors_of_noZeroDivisors

added theorem prod_zero_iff_exists_zero