Theorem associated_abs_left_iff

Modification history

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