Commit 2023-08-03 05:30 4412853e

View on Github →

chore(Mathlib/LinearAlgebra/Basis): Move results about vector spaces to a new file (#6321) This breaks a dependency cycle with Module.Free, which means we can immediately show that all vector spaces are free modules. The lemmas are moved without modification in this PR. A subsequent PR can use the Module.Free results to golf the vector space ones, and deduplicate the API.

Estimated changes

deleted theorem Basis.coe_extend
deleted theorem Basis.coe_ofVectorSpace
deleted theorem Basis.exists_basis
deleted theorem Basis.extend_apply_self
deleted theorem Basis.range_extend
deleted theorem Basis.range_ofVectorSpace
deleted theorem Basis.subset_extend
deleted theorem LinearMap.exists_extend
deleted theorem Submodule.exists_isCompl
deleted theorem VectorSpace.card_fintype
deleted theorem atom_iff_nonzero_span
deleted theorem nonzero_span_atom
deleted theorem quotient_prod_linearEquiv
added theorem Basis.coe_extend
added theorem Basis.exists_basis
added theorem Basis.range_extend
added theorem Basis.subset_extend
added theorem atom_iff_nonzero_span
added theorem nonzero_span_atom