span_coe_eq_restrictScalars — Mathlib

English

For a submodule p ⊆ M, the span over S of p (as a subset of M) equals p viewed as an S-submodule (i.e., p restricted along S).

Русский

Для подмодуля p ⊆ M, порожденное кольцом S в виде множества p равно p, расценённому как S-подмодуль (ограничение по скалярам).

LaTeX

$$$\operatorname{span}_S(p) = p^{\uparrow S}$$$

Lean4

/-- A version of `Submodule.span_eq` for when the span is by a smaller ring. -/
@[simp]
theorem span_coe_eq_restrictScalars [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :
    span S (p : Set M) = p.restrictScalars S :=
  span_eq (p.restrictScalars S)

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