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

'PaperToLean.FletcherPowell.symmetric' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FletcherPowell.add_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FletcherPowell.smul_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FletcherPowell.secant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FletcherPowell.completed_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.FletcherPowell.positive_definite' depends on axioms: [propext, Classical.choice, Quot.sound]