# Book XXIV ch.4, BasisDimension.lean: compiler output, run by the author on 2026-11-03, first run, no edits after writing
# command: cd ~/Desktop/geometry && lake env lean book24/BasisDimension.lean 2>&1 | tee book24/basisdimension.axioms.txt
# result: no errors, no warnings; 14 theorems; none depends on sorryAx
'Book24Basis.indep_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.lemma1' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.single_vector_not_span_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.control_dependent_family' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.lemma2' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.theorem3' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.theorem5a' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.theorem5b' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.theorem6' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.corollary6' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.theorem7' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.exercise12' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.exercise18' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book24Basis.exercise19' depends on axioms: [propext, Classical.choice, Quot.sound]