∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  IsRelPrime a b →
    UniqueFactorizationMonoid.radical (a * b) =
      UniqueFactorizationMonoid.radical a * UniqueFactorizationMonoid.radical b