matPolyEquiv_map_C — Mathlib

English

The action of matPolyEquiv on M.map C yields C M, i.e., the map that applies C to coefficients commutes with matPolyEquiv.

Русский

Действие matPolyEquiv на M.map C даёт C M; отображение коэффициентов через C коммутирует с matPolyEquiv.

LaTeX

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

Lean4

@[simp]
theorem matPolyEquiv_map_C (M : Matrix n n R) : matPolyEquiv (M.map C) = C M := by
  rw [← matPolyEquiv_symm_C, AlgEquiv.apply_symm_apply]

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