∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [inst_3 : Subsingleton Mˣ] [Subsingleton Nˣ] [inst_5 : UniqueFactorizationMonoid M] [UniqueFactorizationMonoid N]
  {m p : M} {n : N},
  m ≠ 0 →
    n ≠ 0 →
      ∀ (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m) {d : { l // l ∣ m } ≃ { l // l ∣ n }},
        (∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') → emultiplicity (↑(d ⟨p, ⋯⟩)) n = emultiplicity p m