Commit 2024-07-15 21:27 f3e70deb

refactor(Mathlib/Algebra/ContinuedFractions/*): generalize determinant formula for continued fraction computation to simple continued fraction (#13555) Determinant formula for continued fractions in Mathlib is specialized for continued fraction computation:

theorem GenContFract.determinant (not_terminated_at_n : ¬(of v).TerminatedAt n) :
    (of v).numerators n * (of v).denominators (n + 1) -
      (of v).denominators n * (of v).numerators (n + 1) = (-1) ^ (n + 1) :=
  determinant_aux <| Or.inr <| not_terminated_at_n

This formula can be generalized for arbitrary simple continued fractions, so we generalize:

theorem SimpContFract.determinant (not_terminatedAt_n : ¬(↑s : GenContFract K).TerminatedAt n) :
    (↑s : GenContFract K).nums n * (↑s : GenContFract K).dens (n + 1) -
      (↑s : GenContFract K).dens n * (↑s : GenContFract K).nums (n + 1) = (-1) ^ (n + 1)

Also, this PR renames Real.exists_genContFract_convs_eq_rat to Real.exists_convs_eq_rat which is forgotten to rename in #13210.