span_eq_toSubmodule — Mathlib

English

Span of a set equals its associated Submodule in the star context.

Русский

Объем образа множества через Span равен соответствующему Submodule в звездном контексте.

LaTeX

$$$$ Submodule.span R (s : Set A) = s.toSubmodule $$$$

Lean4

@[simp]
theorem span_eq_toSubmodule {R} [CommSemiring R] [Module R A] (s : NonUnitalStarSubalgebra R A) :
    Submodule.span R (s : Set A) = s.toSubmodule := by simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

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