Theorems · Definition · commutative algebra

mkFactorOrderIsoOfFactorDvdEquiv

{M : Type u_1} →
  [inst : CommMonoidWithZero M] →
    {N : Type u_2} →
      [inst_1 : CommMonoidWithZero N] →
        [Subsingleton Mˣ] →
          [Subsingleton Nˣ] →
            {m : M} →
              {n : N} →
                {d : { l // l ∣ m } ≃ { l // l ∣ n }} →
                  (∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l') →
                    ↑(Set.Iic (Associates.mk m)) ≃o ↑(Set.Iic (Associates.mk n))

The order isomorphism between the factors of mk m and the factors of mk n induced by a bijection between the factors of m and the factors of n that preserves ∣.

Defined in

Mathlib.RingTheory.ChainOfDivisors

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroCommMonoidWithZeroSubsingletonSubsingleton