Theorem Zsqrtd.ofNat_im

Modification history

2025-09-01 21:59
Mathlib/NumberTheory/Zsqrtd/Basic.lean
refactor: correct names of Zsqrtd lemmas (#29191) …
Deleted Zsqrtd.ofNat_imView on Github →
2025-01-07 09:21
Mathlib/NumberTheory/Zsqrtd/Basic.lean
chore(*): replace `no_index (ofNat n)` with `ofNat(n)` everywhere (#20521) …
Modified Zsqrtd.ofNat_imView on Github →
2023-07-13 01:24
Mathlib/NumberTheory/Zsqrtd/Basic.lean
chore: bump to nightly-2023-07-01 (#5409) …
Modified Zsqrtd.ofNat_imView on Github →
2023-03-30 05:03
Mathlib/NumberTheory/Zsqrtd/Basic.lean
feat(NumberTheory/Zsqrtd/Basic) Lemmas about ofNat (#3052)
Added Zsqrtd.ofNat_imView on Github →