Theorem Algebra.norm_self

Modification history

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