Revision #2956 → #3446 · back to history
45ebd4e89291| Field | From #2956 | To #3446 |
|---|---|---|
| note | The equivalence between algebraicity over ℤ and over ℚ follows from `isAlgebraic_iff_isIntegral` (Mathlib.RingTheory.Algebraic.Integral) and clearing denominators; Mathlib's `IsAlgebraic` handles this uniformly. | The equivalence between algebraicity over ℤ and over ℚ follows from `isAlgebraic_iff_isIntegral` and clearing denominators; Mathlib's `IsAlgebraic` handles this uniformly. |