addLinearEquiv_apply_snd

Mathlib.RingTheory.Polynomial.DegreeLT

URI: https://scilib.ai/kg/mathlib#Polynomial.degreeLT.addLinearEquiv_apply_snd

English

For f ∈ R[X]_{m+n}, the second component equals f / X^m.

Русский

Для f ∈ R[X]_{m+n}, второй компонент равен f / X^m.

LaTeX

$$$\\text{(addLinearEquiv } R\\,m\\,n\\ f).2 = f \\/\\! (X^m).$$$

Lean4

theorem addLinearEquiv_apply_snd {R : Type*} [Ring R] (f) : ((addLinearEquiv R m n f).2 : R[X]) = f /ₘ (X ^ m) :=
  (addLinearEquiv_apply' f).2

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

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

Разделы

Аффилиация

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