radical_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem radical_inf : radical (I ⊓ J) = radical I ⊓ radical J :=
  le_antisymm (le_inf (radical_mono inf_le_left) (radical_mono inf_le_right)) fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
    ⟨m + n, (pow_add r m n).symm ▸ I.mul_mem_right _ hrm, (pow_add r m n).symm ▸ J.mul_mem_left _ hrn⟩

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