single_swap

Mathlib.Data.Finsupp.Single

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

English

For any a1, a2 ∈ α and b ∈ M, single a1 b a2 = single a2 b a1.

Русский

Для любых a1, a2 ∈ α и b ∈ M выполняется single a1 b a2 = single a2 b a1.

LaTeX

$$$\mathrm{single}(a_1,b)(a_2) = \mathrm{single}(a_2,b)(a_1)$$$

Lean4

theorem single_swap (a₁ a₂ : α) (b : M) : single a₁ b a₂ = single a₂ b a₁ := by
  classical simp only [single_apply, eq_comm]

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

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

Разделы

Аффилиация

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