append_comm

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.append_comm

English

Appending two Sym terms commutes up to the natural cast by addition.

Русский

Сложение двух Sym-термов коммутирует с помощью естественного приведения сложения.

LaTeX

$$$ s.\\append s' = \\mathrm{cast}_{\\mathrm{add\\_comm}}(s'.\\append s) $$$

Lean4

theorem append_comm (s : Sym α n') (s' : Sym α n') : s.append s' = Sym.cast (add_comm _ _) (s'.append s) := by
  simp [append, add_comm]

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

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

Разделы

Аффилиация

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