Commit 2025-01-31 14:57 d7d3fa62

View on Github →

chore(NonZeroDivisors): don't import rings (#20871) See https://github.com/leanprover-community/mathlib3/pull/11211 for the copyright header of the new file

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

deleted theorem dvd_cancel_left_coe_nonZeroDivisors

deleted theorem dvd_cancel_left_mem_nonZeroDivisors

deleted theorem dvd_cancel_right_coe_nonZeroDivisors

deleted theorem dvd_cancel_right_mem_nonZeroDivisors

deleted theorem isUnit_iff_mem_nonZeroDivisors_of_finite

deleted theorem mul_cancel_left_coe_nonZeroDivisors

deleted theorem mul_cancel_left_mem_nonZeroDivisors

deleted theorem mul_cancel_right_coe_nonZeroDivisors

deleted theorem mul_cancel_right_mem_nonZeroDivisors

Created Mathlib/Algebra/Ring/NonZeroDivisors.lean

added theorem dvd_cancel_left_coe_nonZeroDivisors

added theorem dvd_cancel_left_mem_nonZeroDivisors

added theorem dvd_cancel_right_coe_nonZeroDivisors

added theorem dvd_cancel_right_mem_nonZeroDivisors

added theorem isUnit_iff_mem_nonZeroDivisors_of_finite

added theorem mul_cancel_left_coe_nonZeroDivisors

added theorem mul_cancel_left_mem_nonZeroDivisors

added theorem mul_cancel_right_coe_nonZeroDivisors

added theorem mul_cancel_right_mem_nonZeroDivisors

Modified Mathlib/FieldTheory/RatFunc/Defs.lean