map_expand

Mathlib.Algebra.MvPolynomial.Expand

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

English

Mapping commutes with expansion: map f (expand p φ) = expand p (map f φ).

Русский

Отображение сохраняет расширение: map f (expand p φ) = expand p (map f φ).

LaTeX

$$$$ map\ f\ (expand\ p\ φ) = expand\ p\ (map\ f\ φ). $$$$

Lean4

@[simp]
theorem map_expand (f : R →+* S) (p : ℕ) (φ : MvPolynomial σ R) : map f (expand p φ) = expand p (map f φ) := by
  simp [expand, map_bind₁]

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

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

Разделы

Аффилиация

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