units_smul_span_eq_top — Mathlib

English

If the span of v is the top submodule, then for any map w:ι → units R, the span of w • v is the top.

Русский

Если порождающее множество v порождает верхний подпространственный предел, то для любой w:ι → единицы кольца R порождающее множество w • v также даёт верхний предел.

LaTeX

$$Submodule.span R (Set.range v) = \top \Rightarrow Submodule.span R (Set.range (instHSMul.hSMul w v)) = \top$$

Lean4

theorem units_smul_span_eq_top {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) {w : ι → Rˣ} :
    Submodule.span R (Set.range (w • v)) = ⊤ :=
  groupSMul_span_eq_top hv

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