baseChange — Mathlib

English

The repr in the base-changed basis of an element x ⊗ y is the scalar action of y on x expressed in the new basis.

Русский

Показатель в базисе изменения базы на элементе x ⊗ y даётся как скалярное действие y на x в новом базисе.

LaTeX

$$$ (b.baseChange S).repr (x \otimes y) i = (b.repr(y))(i) \cdot x $$$

Lean4

/-- The lift of an `R`-basis of `M` to an `S`-basis of the base change `S ⊗[R] M`. -/
noncomputable def baseChange (b : Basis ι R M) : Basis ι S (S ⊗[R] M) :=
  (tensorProduct (.singleton Unit S) b).reindex (Equiv.punitProd ι)

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