Theorem Squarefree.associated_of_isSquare_mul

Modification history

2026-08-19 10:07
Mathlib/Algebra/Squarefree/Basic.lean
feat(Algebra/Squarefree): add exists_sq_mul_squarefree (#42319) …
Added Squarefree.associated_of_isSquare_mulView on Github →