Squarefreeness and multiplicative equivalences #
A candidate for Mathlib.Algebra.Squarefree.Basic: a multiplicative equivalence preserves and
reflects squarefreeness (MulEquiv.squarefree_iff), as it does irreducibility
(MulEquiv.irreducible_iff) and primality (MulEquiv.prime_iff).
theorem
MulEquiv.squarefree_iff
{M : Type u_1}
{N : Type u_2}
{F : Type u_3}
[Monoid M]
[Monoid N]
[EquivLike F M N]
[MulEquivClass F M N]
(f : F)
{x : M}
: