AffineSpace class

Stream: Is there code for X?

[Tomas Skrivan]

Why is there no AffineSpace class? I'm expecting something like:

class AffineSpace (K A : Type) (V : outParam (Type)) [Field K] [AddCommGroup V] [Module K V] where
   diff : A -> A -> V
   vadd : A -> V -> A
   ... some properties about diff and vadd

There is AlgebraicGeometry.AffineSpace but I know nothing about algebraic geometry so that definition does not make any sense to me.

I want to talk about submatrices with dimensions m' and n' that are submatrices of a larger matrix with dimensions m and n. I feel that the natural way of talking about mathematical properties of such submatrices would through affine spaces.

My goal is to differentiate expressions involving submatrices, I could probably use the theory of manifolds bit it feels to be unnecessarily heavy machinery.

(I'm not talking about mathlib matrices here but about my own matrix type that actually holds the data)

[Yuyang Zhao]

docs#AddTorsor (and a scoped notation docs#Affine.termAffineSpace)

[Tomas Skrivan]

Ahh now I understand why AffineSpace in the doc string of AffineSubspace is not a link.