Theorem mem_nonZeroDivisor_of_injective

Modification history

2025-02-04 10:52
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
chore: rename mem_nonZeroDivisor_of_injective and comap_nonZeroDivisor_le_of_injective (#21408)
Deleted mem_nonZeroDivisor_of_injectiveView on Github →
2025-01-22 16:20
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
feat(Algebra/GroupWithZero): `N⁰.comap f ≤ M⁰` for an injective `f : M →*₀ N` (#20955) …
Added mem_nonZeroDivisor_of_injectiveView on Github →