Commit 2025-02-14 14:20 854a2aad

View on Github →

chore(NonZeroDivisors): clean up (#21288) Follow-up to #20871, which was only code moves.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

modified theorem IsUnit.mem_nonZeroDivisors

modified theorem MulEquivClass.map_nonZeroDivisors

modified theorem comap_nonZeroDivisors_le_of_injective

modified theorem eq_zero_of_ne_zero_of_mul_left_eq_zero

modified theorem eq_zero_of_ne_zero_of_mul_right_eq_zero

modified theorem le_nonZeroDivisors_of_noZeroDivisors

modified theorem map_le_nonZeroDivisors_of_injective

modified theorem map_mem_nonZeroDivisors

modified theorem map_ne_zero_of_mem_nonZeroDivisors

modified theorem mem_nonZeroDivisorsLeft_iff

modified theorem mem_nonZeroDivisorsRight_iff

modified theorem mem_nonZeroDivisors_iff

modified theorem mem_nonZeroDivisors_iff_ne_zero

modified theorem mem_nonZeroDivisors_of_injective

modified theorem mem_nonZeroDivisors_of_ne_zero

modified theorem mem_nonZeroSMulDivisors_iff

modified theorem mul_left_coe_nonZeroDivisors_eq_zero_iff

modified theorem mul_left_mem_nonZeroDivisors_eq_zero_iff

modified theorem mul_mem_nonZeroDivisors

modified theorem mul_right_coe_nonZeroDivisors_eq_zero_iff

modified theorem mul_right_mem_nonZeroDivisors_eq_zero_iff

modified theorem nmem_nonZeroDivisorsLeft_iff

modified theorem nmem_nonZeroDivisorsRight_iff

modified theorem nmem_nonZeroDivisors_iff

modified theorem nonZeroDivisors.coe_ne_zero

modified theorem nonZeroDivisors.ne_zero

modified def nonZeroDivisors

modified theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective

modified def nonZeroSMulDivisors

modified theorem powers_le_nonZeroDivisors_of_noZeroDivisors

modified theorem zero_not_mem_nonZeroDivisors