Theorem Zsqrtd.sub_re

Modification history

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