spanFinset_coe — Mathlib

English

The span of a finite set mapped into K, when viewed as a submodule over R, coincides with the standard span: the underlying submodule equals Submodule.span R (f '' s).

Русский

Область определения через конечный образ множества совпадает с обычным порождающим подмодулем: подсистема равна Submodule.span R (f '' s).

LaTeX

$$$ (\operatorname{spanFinset} \; R_1\; s\; f : \FractionalIdeal R_1^0 K) = \text{Submodule}.span R_1 (f '' s) $$$

Lean4

@[simp]
theorem spanFinset_coe {ι : Type*} (s : Finset ι) (f : ι → K) :
    (spanFinset R₁ s f : Submodule R₁ K) = Submodule.span R₁ (f '' s) :=
  rfl

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