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

Modified src/number_theory/pell_matiyasevic.lean

deleted theorem pell.is_pell_conj

added theorem pell.is_pell_iff_mem_unitary

modified theorem pell.is_pell_norm

added theorem pell.is_pell_star

modified theorem pell.pell_zd_sub

Modified src/number_theory/zsqrtd/basic.lean

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

Modified src/number_theory/zsqrtd/gaussian_int.lean

modified theorem gaussian_int.div_def

added theorem gaussian_int.to_complex_star