English
Let α be a field with a linear order, a strict ordered ring structure, and a Floor operation. For every rational x, the fractional part of x, when embedded into α, equals the fractional part of x viewed inside α; i.e. the cast of fract(x) from ℚ to α equals fract(x) computed in α.
Русский
Пусть α — поле с линейным порядком, строгим упорядоченным кольцом и операцией floor. Для любого рационального числа x дробная часть x, затем отображаемая в α, равна дробной части x, вычисленной в α; то есть отражение fract(x) из ℚ в α равно fract(x) в α.
LaTeX
$$$$ ( \\mathrm{fract} \\, x )^{\\uparrow} = \\mathrm{fract}( x^{\\uparrow} ), \\quad x \\in \\mathbb{Q}. $$$$
Lean4
@[simp, norm_cast]
theorem cast_fract (x : ℚ) : (↑(fract x) : α) = fract (x : α) := by
simp only [fract, cast_sub, cast_intCast, floor_cast]
