Theorem zsqrtd.mul_conj
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.mul_conjView on Github →2020-05-27 07:09
src/data/zsqrtd/basic.lean
chore(*): split long lines, unindent in namespaces (#2834) …
Modified zsqrtd.mul_conjView on Github →