Commit 2026-10-28 01:55 af9bba6e

feat(LinearAlgebra/Matrix/GeneralLinearGroup/Defs): add MulEquiv for GL (#43945) Following the API in Data/Matrix/Basic I add :

• the MulEquiv : GL n R ≃* GL n Sinduced by a RingEquiv
• the MulEquiv : GL n R ≃* (GL n R)\mop
• the MulEquiv : GL n (ULift.{w} R) ≃* GL n R
• the MulEquiv : GL m R ≃* GL n R for m ≃ n
• the MulEquiv : GL n (Π i, R i) ≃* Π i, GL n (R i)