Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 20:31 1506335d

View on Github →

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.

Estimated changes

deleted def zsqrtd.add
modified theorem zsqrtd.add_def
modified theorem zsqrtd.add_im
modified theorem zsqrtd.add_re
modified theorem zsqrtd.bit0_im
modified theorem zsqrtd.bit0_re
modified theorem zsqrtd.bit1_re
modified def zsqrtd.conj
modified theorem zsqrtd.conj_im
modified theorem zsqrtd.conj_neg
modified theorem zsqrtd.conj_re
deleted theorem zsqrtd.le_refl
deleted def zsqrtd.mul
modified theorem zsqrtd.mul_im
modified theorem zsqrtd.mul_re
deleted def zsqrtd.neg
modified theorem zsqrtd.neg_im
modified theorem zsqrtd.neg_re
added theorem zsqrtd.nonneg.add
deleted theorem zsqrtd.nonneg_add
deleted def zsqrtd.one
deleted def zsqrtd.zero