expand_one_apply

Mathlib.Algebra.MvPolynomial.Expand

URI: https://scilib.ai/kg/mathlib#MvPolynomial.expand_one_apply

← MathLib Explorer

English

Expanding by 1 acts as the identity on polynomials.

Русский

Расширение на 1 действует как тождество на полиномах.

LaTeX

$$$$ \operatorname{expand}(1) = \mathrm{Id}. $$$$

Lean4

theorem expand_one_apply (f : MvPolynomial σ R) : expand 1 f = f := by
  simp only [expand, pow_one, eval₂Hom_eq_bind₂, bind₂_C_left, AlgHom.coe_mk, RingHom.id_apply]

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

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

Разделы

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

Аффилиация

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