Theorem Zsqrtd.decompose

Modification history

2023-12-27 19:56

Mathlib/NumberTheory/Zsqrtd/Basic.lean

chore(NumberTheory/Zsqrtd): use `@[ext]` (#9299) …

Modified Zsqrtd.decompose View on Github →

2023-03-23 13:44

Mathlib/NumberTheory/Zsqrtd/Basic.lean

feat: port NumberTheory.Zsqrtd.Basic (#3034)

Added Zsqrtd.decompose View on Github →