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 theorem IsUnit.mem_nonZeroDivisors
modified theorem map_mem_nonZeroDivisors
modified theorem mem_nonZeroDivisorsLeft_iff
modified theorem mem_nonZeroDivisors_iff
modified theorem mem_nonZeroSMulDivisors_iff
modified theorem mul_mem_nonZeroDivisors
modified theorem nmem_nonZeroDivisors_iff
modified theorem nonZeroDivisors.coe_ne_zero
modified theorem nonZeroDivisors.ne_zero
modified def nonZeroDivisors
modified def nonZeroSMulDivisors