matPolyEquiv_symm_C — Mathlib

English

The inverse of matPolyEquiv sends a constant polynomial matrix CM to the matrix M with coefficients mapped by C.

Русский

Обратное к матPolyEquiv отправляет константную полиномиальную матрицу CM в матрицу M, полученную путём отображения коэффициентов через C.

LaTeX

$$$\\text{matPolyEquiv}.\\mathrm{symm}(C M) = M.map C$$$

Lean4

@[simp]
theorem matPolyEquiv_symm_C (M : Matrix n n R) : matPolyEquiv.symm (C M) = M.map C := by simp [matPolyEquiv]

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