Theorem AlgEquiv.toLinearEquiv_trans

Modification history