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