Commit 2023-12-27 19:56 d2d0dcdf

View on Github →

chore(NumberTheory/Zsqrtd): use @[ext] (#9299) Added @[ext] to definition structure Zsqrtd (d : ℤ). (also added lemma sub_re, sub_im)

Estimated changes

modified theorem Pell.pellZd_succ
modified theorem Zsqrtd.coe_int_val
modified theorem Zsqrtd.decompose
modified theorem Zsqrtd.dmuld
deleted theorem Zsqrtd.ext
modified theorem Zsqrtd.muld_val
modified theorem Zsqrtd.ofInt_eq_coe
modified theorem Zsqrtd.smul_val
modified theorem Zsqrtd.smuld_val
added theorem Zsqrtd.sub_im
added theorem Zsqrtd.sub_re