addLinearEquiv_symm_apply_inl_basis

English

The inverse image of the first component's basis element under the symmetry maps to the X-power basis of the combined space.

Русский

Образ в обратном направлении базисного элемента первого компонента возвращается к базису X^i в суммарном пространстве.

LaTeX

$$$(\\text{addLinearEquiv } R\\,m\\,n).symm (\\text{LinearMap.inl } R\\,\\_\\,\\_ (\\text{basis } R\\,m\\,i)) = \\text{basis } R\\,(m+n)\\,(i.castAdd n).$$$

Lean4

theorem addLinearEquiv_symm_apply_inl_basis (i : Fin m) :
    (addLinearEquiv R m n).symm (LinearMap.inl R _ _ (basis R m i)) = basis R (m + n) (i.castAdd n) :=
  (LinearEquiv.symm_apply_eq _).2 (addLinearEquiv_castAdd i).symm

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