toMvPolynomial_zero

Mathlib.Algebra.Module.LinearMap.Polynomial

URI: https://scilib.ai/kg/mathlib#Matrix.toMvPolynomial_zero

← MathLib Explorer

English

The mv-polynomial associated to the zero matrix is the zero polynomial.

Русский

mv-полином, соответствующий нулевой матрице, равен нулевому полиному.

LaTeX

$$(0 : Matrix m n R).toMvPolynomial = 0$$

Lean4

@[simp]
theorem toMvPolynomial_zero : (0 : Matrix m n R).toMvPolynomial = 0 := by ext;
  simp only [toMvPolynomial, zero_apply, map_zero, Finset.sum_const_zero, Pi.zero_apply]

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

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

Разделы

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

Аффилиация

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