English
The second coordinate of the i-th right basis vector in the product basis equals the i-th basis vector of the right factor.
Русский
Вторая координата i-го правого базисного вектора в произведении равна i-му базисному вектору правого факторa.
LaTeX
$$(b.prod b')(\mathrm{Sum.inr} i).2 = b' i$$
Lean4
theorem groupSMul_span_eq_top {G : Type*} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] {v : ι → M}
(hv : Submodule.span R (Set.range v) = ⊤) {w : ι → G} : Submodule.span R (Set.range (w • v)) = ⊤ :=
by
rw [eq_top_iff]
intro j hj
rw [← hv] at hj
rw [Submodule.mem_span] at hj ⊢
refine fun p hp => hj p fun u hu => ?_
obtain ⟨i, rfl⟩ := hu
have : ((w i)⁻¹ • (1 : R)) • w i • v i ∈ p := p.smul_mem ((w i)⁻¹ • (1 : R)) (hp ⟨i, rfl⟩)
rwa [smul_one_smul, inv_smul_smul] at this
