toMvPolynomial_constantCoeff

Mathlib.Algebra.Module.LinearMap.Polynomial

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

← MathLib Explorer

English

For any f and i, the constant term of f.toMvPolynomial b1 b2 i is zero.

Русский

Для любого f и i константный коэффициент mv-полиномома f.toMvPolynomial b1 b2 i равен 0.

LaTeX

$$constantCoeff (f.toMvPolynomial b1 b2 i) = 0$$

Lean4

@[simp]
theorem toMvPolynomial_constantCoeff (f : M₁ →ₗ[R] M₂) (i : ι₂) : constantCoeff (f.toMvPolynomial b₁ b₂ i) = 0 :=
  Matrix.toMvPolynomial_constantCoeff _ _

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

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

Разделы

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

Аффилиация

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