map_equivFun — Mathlib

English

Let B be a finite-index basis of M over R and f: M ≃ₗ[R] M' be a linear equivalence. Then the equivFun of the mapped basis equals the composition of f.symm with the original equivFun: (b.map f).equivFun = f.symm ∘ b.equivFun.

Русский

Пусть B — база M над R с конечной размерностью индекса и f: M ≃ₗ[R] M' — линейное биекция. Тогда equivFun для базы, полученной через отображение, равен композиции f.symm с исходной equivFun: (b.map f).equivFun = f.symm ∘ b.equivFun.

LaTeX

$$$$ (b.map\, f).equivFun = f^{-1}.trans\; b.equivFun $$$$

Lean4

@[simp]
theorem map_equivFun [Finite ι] (b : Basis ι R M) (f : M ≃ₗ[R] M') : (b.map f).equivFun = f.symm.trans b.equivFun :=
  rfl

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