determinant — Mathlib

English

If g.TerminatedAt n and n ≤ m, then g.TerminatedAt m: termination propagates forward.

Русский

Если g.TerminatedAt n и n ≤ m, то g.TerminatedAt m: прекращение переходит вперед.

LaTeX

$$$$\text{TerminatedAt}(g,n) \land n \le m \Rightarrow \text{TerminatedAt}(g,m).$$$$

Lean4

/-- The determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)`. -/
theorem 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) :=
  determinant_aux <| Or.inr <| not_terminatedAt_n

Похожие утверждения