(d e : Decimal) : Decimal.leB d e ↔ d.toQ ≤ e.toQ

Proved

BookProof.SirkBandLedger.Decimal.leB_iff

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

sirkspectral-theorytimepiece

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

Preamble

-- Generated from ChapterSirkBandLedger.lean — theorem BookProof.SirkBandLedger.Decimal.leB_iff
import Mathlib
import Definitions.Def_ChapterSirkBandLedger
open BookProof.SirkBandLedger
open BookProof.SirkBandLedger.Decimal















open BookProof.SirkCertificateReader
open BookProof.BandEnclosure

Formal statement

theorem BookProof.SirkBandLedger.Decimal.leB_iff (d e : Decimal) : Decimal.leB d e ↔ d.toQ ≤ e.toQ := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterSirkBandLedger.lean

View graph