Commit 2020-06-30 08:06 a143c386

refactor(linear_algebra/affine_space): allow empty affine subspaces (#3219) When definitions of affine spaces and subspaces were added in #2816, there was some discussion of whether an affine subspace should be allowed to be empty. After further consideration of what lemmas need to be added to fill out the interface for affine subspaces, I've concluded that it does indeed make sense to allow empty affine subspaces, with nonempty hypotheses then added for those results that need them, to avoid artificial nonempty hypotheses for other results on affine spans and intersections of affine subspaces that don't depend on any way on affine subspaces being nonempty and can be more cleanly stated if they can be empty. Thus, change the definition to allow affine subspaces to be empty and remove the bundled direction. The new definition of direction (as the vector_span of the points in the subspace, i.e. the submodule.span of the vsub_set of the points) is the zero submodule for both empty affine subspaces and for those consisting of a single point (and it's proved that in the nonempty case it contains exactly the pairwise subtractions of points in the affine subspace). This doesn't generally add new lemmas beyond those used in reproving existing results (including what were previously the add and sub axioms for affine subspaces) with the new definitions. It also doesn't add the complete lattice structure for affine subspaces, just helps enable adding it later.