Theorem Filter.prod_principal_principal

Modification history