Theorem Zsqrtd.coe_int_dvd_coe_int

Modification history

2024-05-28 07:17

Mathlib/NumberTheory/Zsqrtd/Basic.lean

chore: Rename more `coe_nat`/`coe_int` to `natCast`/`intCast` (#13205)

Deleted Zsqrtd.coe_int_dvd_coe_int View on Github →

2023-03-23 13:44

Mathlib/NumberTheory/Zsqrtd/Basic.lean

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

Added Zsqrtd.coe_int_dvd_coe_int View on Github →