Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Clenshaw.lean
SHA-256: b7f90daaff2d13c642c087da8233bd4300098fae162635a381897bf7b20e2379
Result: passed

'PaperToLean.Clenshaw.recurrence_invariant' depends on axioms: [propext, Quot.sound]
'PaperToLean.Clenshaw.cheb_recurrence' depends on axioms: [propext, Quot.sound]
'PaperToLean.Clenshaw.chebyshev_correct' depends on axioms: [propext, Quot.sound]
'PaperToLean.Clenshaw.scaling' depends on axioms: [propext, Quot.sound]
