Theorems · Definition · commutative algebra

UniqueFactorizationMonoid.normalizedFactorsEquiv

{α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [inst_1 : NormalizationMonoid α] →
      [inst_2 : UniqueFactorizationMonoid α] →
        {β : Type u_2} →
          [inst_3 : CommMonoidWithZero β] →
            [inst_4 : NormalizationMonoid β] →
              [inst_5 : UniqueFactorizationMonoid β] →
                {F : Type u_3} →
                  [inst_6 : EquivLike F α β] →
                    [MulEquivClass F α β] →
                      {f : F} →
                        (∀ (x : α), normalize (f x) = f (normalize x)) →
                          (a : α) →
                            { x // x ∈ UniqueFactorizationMonoid.normalizedFactors a } ≃
                              { y // y ∈ UniqueFactorizationMonoid.normalizedFactors (f a) }

If the monoid equiv f : α ≃* β commutes with normalize then, for a : α, it yields a bijection between the normalizedFactors of a and of f a.

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizationMonoidUniqueFactorizationMonoidCommMonoidWithZeroNormalizationMonoidUniqueFactorizationMonoidEquivLikeMulEquivClass