Commit 2024-03-17 21:35 d47822ad

View on Github →

chore(Squarefree): drop a DecidableEq assumption (#11427) Use classical instead

Estimated changes

Modified Mathlib/Algebra/Squarefree/Basic.lean

modified theorem UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors