Bundling `direction` into `affine_subspace`

Stream: maths

[Yury G. Kudryashov]

@Joseph Myers @Patrick Massot What do you think about rewriting the definition of affine_subspace in the following way?

structure affine_subspace (k : Type*) {V : Type*} (P : Type*) [ring k] [add_comm_group V]
    [module k V] [affine_space V P] :=
(carrier : set P)
(direction : submodule k V)
(vadd_mem_iff' : ∀ (p ∈ carrier) (v), v +ᵥ p ∈ carrier ↔ v ∈ direction)
(nonempty' : direction ≠ ⊥ → carrier.nonempty)

This approach allows us to define subspaces with good defeq properties of direction, and is more consistent with what we do for affine_maps. @Joseph Myers I'm sorry if I was the one who advised against bundling direction when you were writing this part of the library.

[Patrick Massot]

This should be fine, as long as you provide a function constructing this from the old definition of course.

[Yury G. Kudryashov]

Of course.

[Joseph Myers]

I think this should mainly just rearrange details of which lemmas are true by rfl and which actually require something to be proved.

[Joseph Myers]

You originally suggested unbundled direction along with allowing empty affine subspaces. When I became convinced that empty affine subspaces were indeed useful, I then moved to unbundled direction along with allowing them (but of course you can bundle direction and still allow empty affine subspaces, via nonempty' as you have above).