Theorem AddChar.toMonoidHomEquiv_symm_one

Modification history