dvd_radical_iff_of_irreducible — Mathlib

English

An irreducible element a divides radical(b) iff it divides b (for b ≠ 0).

Русский

Неразложимая (irreducible) a делит radical(b) тогда и только тогда, когда делит b (при b ≠ 0).

LaTeX

$$$ Irreducible(a) \Rightarrow (b \neq 0 \Rightarrow (a \mid radical(b) \iff a \mid b)) $$$

Lean4

/-- An irreducible `a` divides the radical of `b` if and only if it divides `b` itself.
Note this generalises to radical elements `a`, see `UniqueFactorizationMonoid.dvd_radical_iff`.
-/
theorem dvd_radical_iff_of_irreducible (ha : Irreducible a) (hb : b ≠ 0) : a ∣ radical b ↔ a ∣ b :=
  by
  constructor
  · intro ha
    exact ha.trans radical_dvd_self
  · intro ha'
    obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd hb ha ha'
    exact hc'.dvd.trans (Finset.dvd_prod_of_mem _ (by simpa [mem_primeFactors] using hc))

Похожие утверждения