Mathlib Changelog
v4
Changelog
About
Github
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