expand_one

Mathlib.Algebra.Polynomial.Expand

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

← MathLib Explorer

English

Expanding by 1 acts as the identity:

Русский

Расширение на единицу действует как тождественное отображение:

LaTeX

$$$\operatorname{expand}(R,1) f = f$$$

Lean4

@[simp]
theorem expand_one (f : R[X]) : expand R 1 f = f :=
  Polynomial.induction_on f (fun r => by rw [expand_C]) (fun f g ihf ihg => by rw [map_add, ihf, ihg]) fun n r _ => by
    rw [map_mul, expand_C, map_pow, expand_X, pow_one]

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

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

Разделы

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

Аффилиация

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