Theorem Associated.neg_left_iff

Modification history

2025-05-16 09:35
Mathlib/Algebra/Ring/Associated.lean
feat(RingTheory/Ideal): An ideal of `ℤ` is generated by its norm (#24933) …
Added Associated.neg_left_iffView on Github →