support_smul

Mathlib.Algebra.Polynomial.Coeff

URI: https://scilib.ai/kg/mathlib#Polynomial.support_smul

← MathLib Explorer

English

Multiplying a polynomial by a scalar does not enlarge its support: supp(r • p) ⊆ supp(p).

Русский

Умножение многочлена на скаляр не расширяет опору: supp(r•p) ⊆ supp(p).

LaTeX

$$support (r \\cdot p) ⊆ support p$$

Lean4

theorem support_smul [SMulZeroClass S R] (r : S) (p : R[X]) : support (r • p) ⊆ support p :=
  by
  intro i hi
  rw [mem_support_iff] at hi ⊢
  contrapose! hi
  simp [hi]

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

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

Разделы

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

Аффилиация

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