English
If the span of a family v is the top submodule, then for any group-valued map w, the span of w • v is also the top submodule.
Русский
Если порождающее множество v заполняет верхний подпространство, то для любого отображения w со значениями в группе порождающее множество w • v тоже задаёт верхний подпространственный предел.
LaTeX
$$Submodule.span R (Set.range v) = \top \Rightarrow Submodule.span R (Set.range (w \cdot v)) = \top$$
Lean4
/-- Given a basis `v` and a map `w` such that for all `i`, `w i` are elements of a group,
`groupSMul` provides the basis corresponding to `w • v`. -/
def groupSMul {G : Type*} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M]
[SMulCommClass G R M] (v : Basis ι R M) (w : ι → G) : Basis ι R M :=
Basis.mk (LinearIndependent.group_smul v.linearIndependent w) (groupSMul_span_eq_top v.span_eq).ge
