image_vsub_product

Mathlib.Algebra.Group.Pointwise.Finset.Scalar

URI: https://scilib.ai/kg/mathlib#Finset.image_vsub_product

English

The image of s × t under the map (· -ᵥ ·) equals s -ᵥ t.

Русский

Образ пары (s, t) под отображением (· -ᵥ ·) равен s -ᵥ t.

LaTeX

$$$ \operatorname{image}_2 (\,\cdot -ᵥ \cdot\,)\; s \; t = s -ᵥ t $$$

Lean4

@[simp]
theorem image_vsub_product : image₂ (· -ᵥ ·) s t = s -ᵥ t :=
  rfl

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

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

Разделы

Аффилиация

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