sym2Mul_apply_mk

Mathlib.Data.Sym.Sym2.Finsupp

URI: https://scilib.ai/kg/mathlib#Finsupp.sym2Mul_apply_mk

English

For p = (a,b), the Sym2 multiplication of f applied to mk p equals f(a) · f(b).

Русский

Для p=(a,b) умножение sym2 для f на mk p равно f(a)·f(b).

LaTeX

$$$f.\mathrm{sym2Mul}(.mk(p)) = f(p.1) \cdot f(p.2)$$$

Lean4

theorem sym2Mul_apply_mk (p : α × α) : f.sym2Mul (.mk p) = f p.1 * f p.2 :=
  rfl

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

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

Разделы

Аффилиация

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