toMvPolynomial_zero

Mathlib.Algebra.Module.LinearMap.Polynomial

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

← MathLib Explorer

English

If M is the zero linear map M1 → M2, then (0).toMvPolynomial b1 b2 = 0.

Русский

Если M1 → M2 тождественно равна нулю, то (0).toMvPolynomial b1 b2 = 0.

LaTeX

$$(0 : M1 →ₗ[R] M2).toMvPolynomial b1 b2 = 0$$

Lean4

@[simp]
theorem toMvPolynomial_zero : (0 : M₁ →ₗ[R] M₂).toMvPolynomial b₁ b₂ = 0 := by unfold toMvPolynomial;
  simp only [map_zero, Matrix.toMvPolynomial_zero]

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

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

Разделы

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

Аффилиация

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