dvd_radical_iff — Mathlib

English

If a and b are coprime, then divRadical(a) and divRadical(b) are coprime.

Русский

Если a и b взаимно просты, то divRadical(a) и divRadical(b) взаимно просты.

LaTeX

$$$\text{IsCoprime}(\operatorname{divRadical}(a), \operatorname{divRadical}(b))$$$

Lean4

/-- 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`.
-/
theorem dvd_radical_iff (ha : IsRadical a) (hb₀ : b ≠ 0) : a ∣ radical b ↔ a ∣ b :=
  by
  refine ⟨fun ha' ↦ ha'.trans radical_dvd_self, fun hab ↦ ?_⟩
  obtain rfl | ha₀ := eq_or_ne a 0
  · simp_all
  · exact (ha.dvd_radical ha₀).trans (radical_dvd_radical hab hb₀)

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