Theorem zsqrtd.conj_mul
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_mulView on Github →2020-07-06 14:12
src/data/zsqrtd/basic.lean
refactor(*): replace nonzero with nontrivial (#3296) …
Modified zsqrtd.conj_mulView on Github →2020-05-27 07:09
src/data/zsqrtd/basic.lean
chore(*): split long lines, unindent in namespaces (#2834) …
Modified zsqrtd.conj_mulView on Github →