Theorems · Theorem · commutative algebra

mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors

∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {N : Type u_2} [inst_2 : CommMonoidWithZero N]
  [inst_3 : Subsingleton Mˣ] [inst_4 : Subsingleton Nˣ] [inst_5 : UniqueFactorizationMonoid M]
  [inst_6 : 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') →
          ↑(d ⟨p, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors n

Defined in

Mathlib.RingTheory.ChainOfDivisors

Cited by

1 results in Mathlib

Foundations

Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroIsCancelMulZeroCommMonoidWithZeroSubsingletonSubsingletonUniqueFactorizationMonoidUniqueFactorizationMonoid