Theorem AlgEquiv.toUnder_hom_right_apply

Modification history