Prove2Me

{L : List BandRecord} {m : ℕ} (hm : L.length - 1 ≤ m) : recAt L m = recAt L (L.length - 1)

Proved
BookProof.SirkBandLedger.recAt_of_ge

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

sirkspectral-theorytimepiece

Lean 4 theorem BookProof.SirkBandLedger.recAt_of_ge (module BookProof.SirkBandLedger), source chapter BookProof/ChapterSirkBandLedger.lean.

Preamble
-- Generated from ChapterSirkBandLedger.lean — theorem BookProof.SirkBandLedger.recAt_of_ge
import Mathlib
import Definitions.Def_ChapterSirkBandLedger
open BookProof.SirkBandLedger















open BookProof.SirkCertificateReader
open BookProof.BandEnclosure
Formal statement
theorem BookProof.SirkBandLedger.recAt_of_ge {L : List BandRecord} {m : ℕ} (hm : L.length - 1 ≤ m) :
    recAt L m = recAt L (L.length - 1) := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterSirkBandLedger.lean

View graph