English
For e a basis over R2 and w a map to units, the i-th coordinate of the units-smul basis equals (w i)^{-1} times e.coord i.
Русский
Для e — базиса над R2 и w:ι → Units R2, i-я координата в coord units-smul равна (w i)^{-1} умножить на e.coord i.
LaTeX
$$(e.unitsSMul w).coord i = (w i)^{-1} \cdot e.coord i$$
Lean4
@[simp]
theorem coord_unitsSMul (e : Basis ι R₂ M) (w : ι → R₂ˣ) (i : ι) : (unitsSMul e w).coord i = (w i)⁻¹ • e.coord i := by
classical
apply e.ext
intro j
trans ((unitsSMul e w).coord i) ((w j)⁻¹ • (unitsSMul e w) j)
· simp [Basis.unitsSMul, ← mul_smul]
simp only [Basis.coord_apply, LinearMap.smul_apply, Basis.repr_self, Units.smul_def, map_smul, Finsupp.single_apply]
split_ifs with h <;> simp [h]
