Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.dvd_radical_iff

∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, IsRadical a → b ≠ 0 → (a ∣ UniqueFactorizationMonoid.radical b ↔ a ∣ b)

If a is a radical element, then a divides the radical of b if and only if it divides b. Note the forward implication holds without the b ≠ 0 assumption via radical_dvd_self.

Defined in

Mathlib.RingTheory.Radical.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroNormalizationMonoidUniqueFactorizationMonoid