Theorem GaussianInt.normSq_le_normSq_of_re_le_of_im_le

Modification history

2023-06-22 07:23
Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)
Added GaussianInt.normSq_le_normSq_of_re_le_of_im_leView on Github →