mul_eq_inf_of_coprime — Mathlib

English

If I ⊔ J = ⊤, then I J = I ⊓ J.

Русский

Если суммы идеалов I ⊔ J = ⊤, то произведение IJ равно их пересечению I ⊓ J.

LaTeX

$$$ IJ = I \cap J \quad \text{if } I \sqcup J = 1. $$$

Lean4

theorem mul_eq_inf_of_coprime (h : I ⊔ J = ⊤) : I * J = I ⊓ J :=
  le_antisymm mul_le_inf fun r ⟨hri, hrj⟩ =>
    let ⟨s, hsi, t, htj, hst⟩ := Submodule.mem_sup.1 ((eq_top_iff_one _).1 h)
    mul_one r ▸ hst ▸ (mul_add r s t).symm ▸ Ideal.add_mem (I * J) (mul_mem_mul_rev hsi hrj) (mul_mem_mul hri htj)

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