Theorem zsqrtd.conj_re
Modification history
2023-03-12 20:39
src/number_theory/zsqrtd/basic.lean
refactor(number_theory/zsqrtd): replace `zsqrtd.conj` with `star` (#18572) …
Deleted zsqrtd.conj_reView on Github →2022-04-14 20:31
src/number_theory/zsqrtd/basic.lean
chore(number_theory/zsqrtd/*): Missing docstrings and cleanups (#13445) …
Modified zsqrtd.conj_reView on Github →2020-05-27 07:09
src/data/zsqrtd/basic.lean
chore(*): split long lines, unindent in namespaces (#2834) …
Modified zsqrtd.conj_reView on Github →