English
The rational numbers ℚ form a number field; in particular, ℚ is a field, char 0, finite-dimensional over itself.
Русский
Рациональные числа ℚ образуют число поле: характеристика 0 и конечнократно размерно над собой.
LaTeX
$$$\\mathbb{Q} \\text{ is a number field; in particular } \\mathbb{Q} \\text{ has finite dimension over itself.}$$$
Lean4
instance numberField : NumberField ℚ where
to_charZero := inferInstance
to_finiteDimensional := by
-- The vector space structure of `ℚ` over itself can arise in multiple ways:
-- all fields are vector spaces over themselves (used in `Rat.finiteDimensional`)
-- all char 0 fields have a canonical embedding of `ℚ` (used in `NumberField`).
-- Show that these coincide:
convert (inferInstance : FiniteDimensional ℚ ℚ)
