addLinearEquiv_symm_apply — Mathlib

English

The image of i.castAdd n under basisProd corresponds to (basis R n i, 0) in the product basis.

Русский

Образ i.castAdd n под basisProd соответствует (basis R n i, 0) в произведенном базисе.

LaTeX

$$$\\text{basisProd } R\\,m\\,n (i.castAdd n) = (\\text{basis } R\\,n\\,i, 0).$$$

Lean4

theorem addLinearEquiv_symm_apply (PQ) :
    ((addLinearEquiv R m n).symm PQ : R[X]) = (PQ.1 : R[X]) + (PQ.2 : R[X]) * X ^ (m : ℕ) :=
  calc
    _ = ((addLinearEquiv R m n).symm (LinearMap.inl R _ _ PQ.1 + LinearMap.inr R _ _ PQ.2) : R[X]) := by
      rw [LinearMap.inl_apply, LinearMap.inr_apply, Prod.add_def, add_zero, zero_add]
    _ = _ := by rw [map_add, Submodule.coe_add, addLinearEquiv_symm_apply_inl, addLinearEquiv_symm_apply_inr]

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