Theorem Equiv.toFun_inducedStructureEquiv

Modification history