mathlib
2af08364
- refactor(number_theory/zsqrtd): replace `zsqrtd.conj` with `star` (#18572)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
refactor(number_theory/zsqrtd): replace `zsqrtd.conj` with `star` (#18572) This allows more existing lemmas to be used; notably, `unitary (zqsrt d)` becomes something we can talk about.
Author
eric-wieser
Parents
c985ae98
Loading