Theorem GaussianInt.norm_pos

Modification history

2023-06-22 07:23

Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

feat: port NumberTheory.Zsqrtd.GaussianInt (#5134)

Added GaussianInt.norm_pos View on Github →