mathlib
ff027743 - feat(algebra/squarefree): norm_num extension for squarefree (#11666)

Commit
3 years ago
feat(algebra/squarefree): norm_num extension for squarefree (#11666) Adds two methods for computing `squarefree`: an improved algorithm for VM computation of squarefreedom via the `min_sq_fac` function, and a proof procedure which follows the same evaluation strategy as a `norm_num` extension.
Author
Parents
Loading