matPolyEquiv_diagonal_X

Mathlib.RingTheory.MatrixPolynomialAlgebra

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

← MathLib Explorer

English

Applying matPolyEquiv to the diagonal X yields X itself.

Русский

Применение matPolyEquiv к диагонали X возвращает X.

LaTeX

$$$\\text{matPolyEquiv}(\\mathrm{diagonal}(\\mathrm{X})) = \\mathrm{X}$$$

Lean4

@[simp]
theorem matPolyEquiv_diagonal_X : matPolyEquiv (diagonal fun _ : n => (X : R[X])) = X := by
  rw [← matPolyEquiv_symm_X, AlgEquiv.apply_symm_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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