isCoprime_iff_codisjoint — Mathlib

English

IsCoprime I J is equivalent to Codisjoint I J.

Русский

IsCoprime I J эквивалентно Codisjoint I J.

LaTeX

$$$$ IsCoprime(I,J) \iff Codisjoint(I,J) $$$$

Lean4

theorem isCoprime_iff_codisjoint : IsCoprime I J ↔ Codisjoint I J :=
  by
  rw [IsCoprime, codisjoint_iff]
  constructor
  · rintro ⟨x, y, hxy⟩
    rw [eq_top_iff_one]
    apply (show x * I + y * J ≤ I ⊔ J from sup_le (mul_le_left.trans le_sup_left) (mul_le_left.trans le_sup_right))
    rw [hxy]
    simp only [one_eq_top, Submodule.mem_top]
  · intro h
    refine ⟨1, 1, ?_⟩
    simpa only [one_eq_top, top_mul, Submodule.add_eq_sup]

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