mathlib

32fdb81b - feat(data/zsqrtd/to_real): Add `to_real` (#5640)

feat(data/zsqrtd/to_real): Add `to_real` (#5640) Also adds `norm_eq_zero`, and replaces some calls to simp with direct lemma applications Co-authored-by: Johan Commelin <johan@commelin.net>