prod_mk

Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

URI: https://scilib.ai/kg/mathlib#IncidenceAlgebra.prod_mk

English

At coordinates ((a1,b1),(a2,b2)) the product f.prod g equals f(a1,a2) times g(b1,b2).

Русский

В координатах ((a1,b1),(a2,b2)) произведение f.prod g равно f(a1,a2) умножить на g(b1,b2).

LaTeX

$$$ (f.prod g)((a_1,b_1),(a_2,b_2)) = f(a_1,a_2) \cdot g(b_1,b_2) $$$

Lean4

theorem prod_mk (a₁ a₂ : α) (b₁ b₂ : β) : f.prod g (a₁, b₁) (a₂, b₂) = f a₁ a₂ * g b₁ b₂ :=
  rfl

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

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

Разделы

Аффилиация

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