Rat.cast_id

theorem Rat.cast_id : ∀ (n : ℚ), ↑n = n

This theorem asserts that for any rational number 'n', casting 'n' to a rational number results in 'n' itself. In other words, if a variable is already a rational number, casting it as a rational number doesn't change its value.

More concisely: For any rational number 'n', the conversion of 'n' to a rational number yields the same value.