Commit 2025-02-04 10:52 415af18d

View on Github →

chore: rename mem_nonZeroDivisor_of_injective and comap_nonZeroDivisor_le_of_injective (#21408)

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

deleted theorem comap_nonZeroDivisor_le_of_injective

added theorem comap_nonZeroDivisors_le_of_injective

deleted theorem mem_nonZeroDivisor_of_injective

added theorem mem_nonZeroDivisors_of_injective

Modified Mathlib/RingTheory/Artinian/Algebra.lean

Modified Mathlib/RingTheory/LocalRing/Subring.lean