prod_span — Mathlib

English

For a finite set s and a family of subsets I(i) ⊆ R, the product of the spans equals the span of the product: ∏_{i∈s} span(I(i)) = span(∏_{i∈s} I(i)).

Русский

Для конечного множества s и семейства подмножеств I(i) ⊆ R произведение спанов равно спану произведения: ∏_{i∈s} span(I(i)) = span(∏_{i∈s} I(i)).

LaTeX

$$$\prod_{i\in s} \operatorname{span}(I(i)) = \operatorname{span}\left(\prod_{i\in s} I(i)\right)$$$

Lean4

theorem prod_span {ι : Type*} (s : Finset ι) (I : ι → Set R) :
    (∏ i ∈ s, Ideal.span (I i)) = Ideal.span (∏ i ∈ s, I i) :=
  Submodule.prod_span s I

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