leadingCoeff_pow

Mathlib.RingTheory.MvPolynomial.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.leadingCoeff_pow

← MathLib Explorer

English

If f is monic, then f^n is monic for all n.

Русский

Если f моноичен, то f^n моноичен для любого n.

LaTeX

$$$$ m.Monic(f) \Rightarrow m.Monic(f^n) \text{ for all } n. $$$$

Lean4

/-- Leading coefficient of powers (in a reduced ring) -/
theorem leadingCoeff_pow [IsReduced R] (f : MvPolynomial σ R) (n : ℕ) : m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n :=
  by rw [leadingCoeff, degree_pow, coeff_pow_nsmul_degree]

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

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

Разделы

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

Аффилиация

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