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

'PaperToLean.Broyden.action' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.secant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.unchanged_on_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.distance_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.distance_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.pythagorean' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.least_change' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.unique_minimizer' depends on axioms: [propext, Classical.choice, Quot.sound]