English
Let R be a commutative ring, ι a finite index type, and I: ι → ℕ with pairwise coprime values. Then the infimum of the principal ideals generated by I(i) in R equals the principal ideal generated by the product ∏ I(i) (cast to R): ⨅ i (I(i)R) = (∏ i I(i))R.
Русский
Пусть R — коммутативное кольцо, ι — конечное множество индексов, и I(i) ∈ ℕ попарно взаимно просты. Тогда наименьшая общая площадь порожденных ими основных идеалов в R равна основному идеалу, порожденному произведению всех I(i) (в R): ⨅ i (I(i)R) = (∏ i I(i))R.
LaTeX
$$$ \bigcap_{i \in \iota} (I(i)R) = \left( \prod_{i \in \iota} I(i) \right) R. $$$
Lean4
theorem sup_eq_top_iff_isCoprime {R : Type*} [CommSemiring R] (x y : R) :
span ({ x } : Set R) ⊔ span { y } = ⊤ ↔ IsCoprime x y :=
by
rw [eq_top_iff_one, Submodule.mem_sup]
constructor
· rintro ⟨u, hu, v, hv, h1⟩
rw [mem_span_singleton'] at hu hv
rw [← hu.choose_spec, ← hv.choose_spec] at h1
exact ⟨_, _, h1⟩
· exact fun ⟨u, v, h1⟩ => ⟨_, mem_span_singleton'.mpr ⟨_, rfl⟩, _, mem_span_singleton'.mpr ⟨_, rfl⟩, h1⟩
