English
For a basis v and a unit-valued function w, the coordinates of the scaled basis (v.isUnitSMul hw) are scaled by the inverse of the corresponding unit: (v.isUnitSMul hw).repr x i = (hw i).unit^{-1} · v.repr x i.
Русский
Для базиса v и функции w, значения координат базиса, полученного после умножения единицами, равны отношению единицы (обратной к w_i) и исходного представления: (v.isUnitSMul hw).repr x i = (hw i).unit^{-1} · v.repr x i.
LaTeX
$$$(v.\\mathrm{isUnitSMul}(hw)).\\mathrm{repr}\\, x\\, i = (hw\,i).\\mathrm{unit}^{-1} \\cdot v.\\mathrm{repr}\\, x\\, i$$$
Lean4
theorem repr_isUnitSMul {v : Basis ι R₂ M} {w : ι → R₂} (hw : ∀ i, IsUnit (w i)) (x : M) (i : ι) :
(v.isUnitSMul hw).repr x i = (hw i).unit⁻¹ • v.repr x i :=
repr_unitsSMul _ _ _ _
