Commit 2026-11-10 11:56 8d8af1b2

View on Github →

feat: simultaneous Dirichlet approximation theorem (#45646) This is an extension of Real.exists_int_int_abs_mul_sub_le to multiple numbers. The proof is similar.

Estimated changes