English
The default embedding of rationals into a division ring K with NatCast, IntCast, and Div is given by q ↦ (q.num) / (q.den) within K.
Русский
Стандартное включение из полей рациональных чисел в делительную оболочку K задаётся отображением q ↦ (q.num) / (q.den) в K.
LaTeX
$$$\operatorname{castRec}_{K}(q) = \dfrac{q_{\mathrm{num}}}{q_{\mathrm{den}}}$$$
Lean4
/-- The default definition of the coercion `ℚ → K` for a division ring `K`.
`↑q : K` is defined as `(q.num : K) / (q.den : K)`.
Do not use this directly (instances of `DivisionRing` are allowed to override that default for
better definitional properties). Instead, use the coercion. -/
def castRec [NatCast K] [IntCast K] [Div K] (q : ℚ) : K :=
q.num / q.den
