Def GaussianInt.toComplex

Modification history

2023-06-22 07:23

Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

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

Added GaussianInt.toComplex View on Github →