Commit 2025-08-19 14:37 0bb58c27

feat(LinearAlgebra/Projectivization): GL(V) action (#26811) Some API around projective spaces and general linear groups:

• an equiv between V and W gives an equiv between GL(V) and GL(W)
• GL(V) acts on the projectivization of V
• GL 2 K acts on OnePoint K (which is the projectivization of K x K) I am adding these because I need them to define cusps in modular form theory, but they are hopefully something of general usefulness beyond that.