Theorems · Theorem · commutative algebra

divisor_closure_eq_closure

∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [IsCancelMulZero M₀] (x y : M₀),
  x * y ∈ Submonoid.closure {r | IsUnit r ∨ Prime r} → x ∈ Submonoid.closure {r | IsUnit r ∨ Prime r}

Let x, y ∈ M₀. If x * y can be written as a product of units and prime elements, then x can be written as a product of units and prime elements.

Defined in

Mathlib.Algebra.BigOperators.Associated

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZero