Theorem GaussianInt.norm_eq_zero

Modification history

2026-07-29 08:56
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
chore: remove some (triple) underscore soup (#42208) …
Modified GaussianInt.norm_eq_zeroView on Github →
2023-06-22 07:23
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
Added GaussianInt.norm_eq_zeroView on Github →