sup_mul_eq_of_coprime_left — Mathlib

English

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

Русский

Если I ⊔ J = ⊤, то I ⊔ J K = I ⊔ K.

LaTeX

$$$ I \oplus J K = I \oplus K \quad \text{when } I \oplus J = 1. $$$

Lean4

theorem sup_mul_eq_of_coprime_left (h : I ⊔ J = ⊤) : I ⊔ J * K = I ⊔ K :=
  le_antisymm (sup_le_sup_left mul_le_left _) fun i hi =>
    by
    rw [eq_top_iff_one] at h; rw [Submodule.mem_sup] at h hi ⊢
    obtain ⟨i1, hi1, j, hj, h⟩ := h; obtain ⟨i', hi', k, hk, hi⟩ := hi
    refine ⟨_, add_mem hi' (mul_mem_right k _ hi1), _, mul_mem_mul hj hk, ?_⟩
    rw [add_assoc, ← add_mul, h, one_mul, hi]

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