Commit 2023-03-12 20:39 2af08364

View on Github →

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.

Estimated changes

deleted def zsqrtd.conj
deleted theorem zsqrtd.conj_add
deleted theorem zsqrtd.conj_conj
deleted def zsqrtd.conj_hom
deleted theorem zsqrtd.conj_im
deleted theorem zsqrtd.conj_mul
deleted theorem zsqrtd.conj_neg
deleted theorem zsqrtd.conj_one
deleted theorem zsqrtd.conj_re
deleted theorem zsqrtd.conj_sub
deleted theorem zsqrtd.conj_zero
deleted theorem zsqrtd.mul_conj
added theorem zsqrtd.mul_star
modified theorem zsqrtd.norm_conj
modified theorem zsqrtd.norm_eq_mul_conj
added theorem zsqrtd.star_im
added theorem zsqrtd.star_mk
added theorem zsqrtd.star_re