How to prove that the decimal part of a rational number is c

Stream: new members

[tooball]

How to prove that the decimal part of a rational number is cyclic?
If I want to express a decimal place of a rational number, such as the 100th place of 6/7, without using direct calculation, how should I formalize the problem.

[Zhang Qinchuan]

It seems that there is no such thing in Mathlib, just define one yourself.
$6/7=0.\overline{857142}$

import Mathlib

def decimal_after_pt (x : ℚ) (n : ℕ) : ℕ :=
  Nat.floor (x * 10 ^ (n + 1)) % 10

def x : ℚ := 6 / 7

-- [8, 5, 7, 1, 4, 2, 8, 5, 7, 1, 4, 2]
#eval (List.range (6 * 2)).map (decimal_after_pt x ·)