map — Mathlib

English

Given a basis b and a linear equivalence f, the mapped basis b.map f is the basis whose representation is f.symm ∘ b.repr.

Русский

При заданном базисе b и линейном эквиваленте f получаем новый базис b.map f, чья репрезентация равна f.symm ∘ b.repr.

LaTeX

$$$(b.map\ f).repr = f^{-1} \circ b.repr$$$

Lean4

/-- Apply the linear equivalence `f` to the basis vectors. -/
@[simps]
protected def map : Basis ι R M' :=
  ofRepr (f.symm.trans b.repr)

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