HomeIsabelle/Phabricator

changed definition of square-free-factorization: now [(p1,e1),...,(pn,en)]…

Description

changed definition of square-free-factorization: now [(p1,e1),...,(pn,en)] encodes p1^e1 * ... * pn^en
(it was p1^Suc e1 * ... * pn^Suc en before)