Theorem Zsqrtd.bit1_im

Modification history

2024-06-10 07:27
Mathlib/NumberTheory/Zsqrtd/Basic.lean
chore(*): drop some bit0/bit1 lemmas (#13679) …
Deleted Zsqrtd.bit1_imView on Github →
2023-03-23 13:44
Mathlib/NumberTheory/Zsqrtd/Basic.lean
feat: port NumberTheory.Zsqrtd.Basic (#3034)
Added Zsqrtd.bit1_imView on Github →