Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-17 16:20 73922b54

View on Github →

feat(data/zsqrtd/basic): add some lemmas about conj, norm (#6715)

Estimated changes

added theorem zsqrtd.conj_add
added theorem zsqrtd.conj_conj
added def zsqrtd.conj_hom
added theorem zsqrtd.conj_neg
added theorem zsqrtd.conj_one
added theorem zsqrtd.conj_sub
added theorem zsqrtd.conj_zero
added theorem zsqrtd.norm_conj
added theorem zsqrtd.norm_neg