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

'PaperToLean.Kaczmarz.dot_self_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.dot_self_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.row_residual' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.satisfies_row' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.distance_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.relaxed_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.strict_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.fixed_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.system_fixed_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
