Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 18:19 32fdb81b

View on Github →

feat(data/zsqrtd/to_real): Add to_real (#5640) Also adds norm_eq_zero, and replaces some calls to simp with direct lemma applications

Estimated changes

Modified src/data/zsqrtd/basic.lean

added theorem zsqrtd.dmuld

added theorem zsqrtd.hom_ext

added def zsqrtd.lift

added theorem zsqrtd.lift_injective

added theorem zsqrtd.norm_eq_zero

Modified src/data/zsqrtd/gaussian_int.lean

Created src/data/zsqrtd/to_real.lean

added theorem zsqrtd.to_real_injective