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

'PaperToLean.Aitken.determinant_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Aitken.geometric_denominator' depends on axioms: [propext, Quot.sound]
'PaperToLean.Aitken.geometric_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Aitken.geometric_sequence_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Aitken.two_mode_residual' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Aitken.affine_equivariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Aitken.constant_error_is_not_removed' depends on axioms: [propext, Quot.sound]
'PaperToLean.Aitken.normalized_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Aitken.accelerates' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Aitken.preserves_limit' depends on axioms: [propext, Classical.choice, Quot.sound]