restrictScalars_apply — Mathlib

English

For all i, the i-th restricted-scalar basis element equals the original i-th basis element when viewed in M: (b.restrictScalars R i) = b i.

Русский

Пусть для каждого i элемент i-го базиса после ограничения скаляров совпадает с исходным i-ым базисным вектором: (b.restrictScalars R i) = b i.

LaTeX

$$$(b.restrictScalars\\ R\\ i) = b_i$$$

Lean4

@[simp]
theorem restrictScalars_apply (i : ι) : (b.restrictScalars R i : M) = b i := by
  simp only [Basis.restrictScalars, Basis.span_apply]

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