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

'PaperToLean.Shanks.denominator_factor' depends on axioms: [propext, Quot.sound]
'PaperToLean.Shanks.numerator_factor' depends on axioms: [propext, Quot.sound]
'PaperToLean.Shanks.two_mode_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Shanks.sample_shift' depends on axioms: [propext, Quot.sound]
'PaperToLean.Shanks.sequence_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Shanks.single_mode_singular' depends on axioms: [propext, Quot.sound]