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

'PaperToLean.Schulz.right_error_square' depends on axioms: [propext]
'PaperToLean.Schulz.left_error_square' depends on axioms: [propext]
'PaperToLean.Schulz.right_error_exact' depends on axioms: [propext]
'PaperToLean.Schulz.left_error_exact' depends on axioms: [propext]
'PaperToLean.Schulz.nilpotent_right_exact' depends on axioms: [propext]
'PaperToLean.Schulz.inverse_fixed' depends on axioms: [propext]