leadingCoeff_expand

Mathlib.Algebra.Polynomial.Expand

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

← MathLib Explorer

English

For p > 0, (expand R p f).Monic ↔ f.Monic.

Русский

Для p > 0, (expand R p f).Monic эквивалентно f.Monic.

LaTeX

$$$(\expand R p f).Monic \iff f.Monic$$$

Lean4

theorem leadingCoeff_expand {p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).leadingCoeff = f.leadingCoeff := by
  simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]

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

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

Разделы

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

Аффилиация

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