addLinearEquiv — Mathlib

English

There is a linear isomorphism addLinearEquiv between R[X]_{m+n} and R[X]_m × R[X]_n, induced by the two bases and the natural reindexing.

Русский

Существует линейный изоморфизм addLinearEquiv между R[X]_{m+n} и R[X]_m × R[X]_n, индуцируемый двумя базисами и естественным перенумерованием.

LaTeX

$$$R[X]_{m+n} \\cong_R R[X]_m \\times R[X]_n.$$$

Lean4

/-- An isomorphism between `R[X]_(m + n)` and `R[X]_m × R[X]_n` given by the fact that the bases are
both indexed by `Fin (m + n)`. -/
noncomputable def addLinearEquiv : R[X]_(m + n) ≃ₗ[R] R[X]_m × R[X]_n :=
  Basis.equiv (basis ..) (basisProd ..) (Equiv.refl _)

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