Theorem Zsqrtd.sub_im

Modification history

2023-12-27 19:56
Mathlib/NumberTheory/Zsqrtd/Basic.lean
chore(NumberTheory/Zsqrtd): use `@[ext]` (#9299) …
Added Zsqrtd.sub_imView on Github →