radical_mul — Mathlib

English

The radical of the product equals the intersection of radicals: radical(I J) = radical I ∧ radical J.

Русский

Радикал произведения равен пересечению радикалов: √(I J) = √I ∩ √J.

LaTeX

$$$\\operatorname{radical}(I \\cdot J) = \\operatorname{radical}(I) \\cap \\operatorname{radical}(J)$$$

Lean4

theorem radical_mul : radical (I * J) = radical I ⊓ radical J :=
  by
  refine le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ => ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩
  have := radical_mono <| @mul_le_inf _ _ I J
  simp_rw [radical_inf I J] at this
  assumption

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