coeff_pow_of_natDegree_le_of_eq_ite'

Mathlib.Tactic.ComputeDegree

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite'

Lean4

theorem coeff_pow_of_natDegree_le_of_eq_ite' {m n o : ℕ} {a : R} {p : R[X]} (h_pow : natDegree p ≤ n)
    (h_exp : m * n ≤ o) (h_pow_bas : coeff p n = a) : coeff (p ^ m) o = if o = m * n then a ^ m else 0 :=
  by
  split_ifs with h
  · subst h h_pow_bas
    exact coeff_pow_of_natDegree_le ‹_›
  · apply coeff_eq_zero_of_natDegree_lt
    apply lt_of_le_of_lt ?_ (lt_of_le_of_ne ‹_› ?_)
    · exact natDegree_pow_le_of_le m ‹_›
    · exact Iff.mp ne_comm h

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

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

Разделы

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

Аффилиация

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