no duplicates in normalized factors

Stream: Is there code for X?

[Bhavik Mehta]

import Mathlib.RingTheory.Nilpotent.Defs
import Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

open UniqueFactorizationMonoid

variable {M : Type*} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M]

theorem test {a : M} (ha : IsRadical a) : (normalizedFactors a).Nodup := by
  sorry

Do we have this anywhere? I'm struggling to find many lemmas to help with IsRadical

[Junyan Xu]

import Mathlib.Algebra.Squarefree.Basic

open UniqueFactorizationMonoid

variable {M : Type*} [CancelCommMonoidWithZero M] [NormalizationMonoid M] [UniqueFactorizationMonoid M]

theorem test {a : M} (ha : IsRadical a) : (normalizedFactors a).Nodup := by
  obtain rfl | ne := eq_or_ne a 0; · simp
  rwa [← squarefree_iff_nodup_normalizedFactors ne,
    ← isRadical_iff_squarefree_of_ne_zero ne]

[Bhavik Mehta]

Ah, thanks!