coeff_congr

Mathlib.Tactic.ComputeDegree

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

Lean4

theorem coeff_congr (h : coeff f m = r) (natDeg_eq_coeff : m = n) {s : R} (rs : r = s) : coeff f n = s :=
  natDeg_eq_coeff ▸ rs ▸ h

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

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

Разделы

Аффилиация

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