prod_span_singleton — Mathlib

English

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

Русский

Для конечного множества s и функции I: s → 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_singleton {ι : Type*} (s : Finset ι) (I : ι → R) :
    (∏ i ∈ s, Ideal.span ({I i} : Set R)) = Ideal.span {∏ i ∈ s, I i} :=
  Submodule.prod_span_singleton s I

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