# Book XXIV ch.3, VectorSpace.lean: compiler output, run by the author after the smul_mem binder fix
# command: cd ~/Desktop/geometry && lake env lean book24/VectorSpace.lean 2>&1 | tee book24/vectorspace.axioms.txt
# result: no errors, no warnings; 12 theorems; none depends on sorryAx
'Book24VS.zero_unique' depends on axioms: [propext]
'Book24VS.zero_smul_axioms' depends on axioms: [propext, Quot.sound]
'Book24VS.neg_one_smul_eq_neg' depends on axioms: [propext, Quot.sound]
'Book24VS.inter_isSub' depends on axioms: [propext, Quot.sound]
'Book24VS.sum_isSub' depends on axioms: [propext, Quot.sound]
'Book24VS.trivial_isSub' depends on axioms: [propext, Quot.sound]
'Book24VS.cong_refl' depends on axioms: [propext, Quot.sound]
'Book24VS.cong_symm' depends on axioms: [propext, Quot.sound]
'Book24VS.cong_trans' depends on axioms: [propext, Quot.sound]
'Book24VS.cong_add' depends on axioms: [propext, Quot.sound]
'Book24VS.cong_smul' depends on axioms: [propext, Quot.sound]
'Book24VS.control_cong_not_trans' depends on axioms: [propext, Classical.choice, Quot.sound]