unitsSMul_apply — Mathlib

English

For i, the i-th coordinate of the basis obtained by units-smul is w i • v i.

Русский

Для i-й координаты базиса, полученного посредством преобразования единиц, имеем w i • v i.

LaTeX

$$unitsSMul v w i = w i \cdot v i$$

Lean4

theorem unitsSMul_apply {v : Basis ι R M} {w : ι → Rˣ} (i : ι) : unitsSMul v w i = w i • v i :=
  mk_apply (LinearIndependent.units_smul v.linearIndependent w) (units_smul_span_eq_top v.span_eq).ge i

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