mathlib

1506335d - chore(number_theory/zsqrtd/*): Missing docstrings and cleanups (#13445)

chore(number_theory/zsqrtd/*): Missing docstrings and cleanups (#13445) Add docstrings to `gaussian_int` and `zsqrtd.norm` and inline definitions which did not have a docstring nor deserved one.