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

'PaperToLean.Samuelson.centered_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Samuelson.zero_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Samuelson.deviation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Samuelson.equality_when_others_equal' depends on axioms: [propext, Classical.choice, Quot.sound]