matPolyEquiv_symm_X

Mathlib.RingTheory.MatrixPolynomialAlgebra

URI: https://scilib.ai/kg/mathlib#matPolyEquiv_symm_X

English

The inverse matPolyEquiv_symm_X is the diagonal matrix with X on the diagonal.

Русский

Обратное матPolyEquiv.symm_X — диагональная матрица с X на диагонали.

LaTeX

$$$\\text{matPolyEquiv}.\\mathrm{symm}(X) = \\mathrm{diagonal}_{n}(X)$$$

Lean4

@[simp]
theorem matPolyEquiv_symm_X : matPolyEquiv.symm X = diagonal fun _ : n => (X : R[X]) := by
  simp [matPolyEquiv, Matrix.smul_one_eq_diagonal]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru