English
Let b be a basis of a module M over a ring R, indexed by ι. If w : ι → R takes a unit value at every index (i.e., w i is a unit for all i), then the basis obtained by scaling each basis vector by w i, namely the i-th vector equals w i times b i, is again a basis of M. In symbols, for hw(i) = IsUnit(w i), we have (b.isUnitSMul hw) i = w i · b i for all i.
Русский
Пусть b — базис модуля M над кольцом R, индексированный по ι. Пусть w : ι → R так, что для каждого i элемент w i является единицей, тогда базис, получаемый умножением каждого базисного вектора на w i, то есть i-й вектор равен w i · b i, снова является базисом M.
LaTeX
$$$\\forall i,\ (b.\\mathrm{isUnitSMul}(hw))\\,i = w_i \\cdot b_i$$$
Lean4
/-- A version of `unitsSMul` that uses `IsUnit`. -/
def isUnitSMul (v : Basis ι R M) {w : ι → R} (hw : ∀ i, IsUnit (w i)) : Basis ι R M :=
unitsSMul v fun i => (hw i).unit
