Commit 2023-03-30 05:03 bf43216f

View on Github →

feat(NumberTheory/Zsqrtd/Basic) Lemmas about ofNat (#3052)

Estimated changes

added theorem Zsqrtd.ofNat_im
added theorem Zsqrtd.ofNat_re