Theorem GaussianInt.div_def

Modification history

2023-06-22 07:23

Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean

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

Added GaussianInt.div_def View on Github →