isUnitSMul_apply — Mathlib

English

Let v be a basis of M over R and w : ι → R with each w i a unit. Then the i-th coordinate of the new basis (v.isUnitSMul hw) is w i times the i-th coordinate of v, i.e., (v.isUnitSMul hw) i = w i · (v i).

Русский

Пусть v — базис M над R, а w : ι → R так, что каждый w i является единицей. Тогда i-я координата нового базиса (v.isUnitSMul hw) равна w i умноженному на i-ю координату v: (v.isUnitSMul hw) i = w i · (v i).

LaTeX

$$$\\forall i,\ (v.\\mathrm{isUnitSMul}(hw))\\,i = w_i \\cdot (v\\,i) $$$

Lean4

theorem isUnitSMul_apply {v : Basis ι R M} {w : ι → R} (hw : ∀ i, IsUnit (w i)) (i : ι) :
    v.isUnitSMul hw i = w i • v i :=
  unitsSMul_apply i

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