image2_vsub

Mathlib.Algebra.Group.Pointwise.Set.Scalar

URI: https://scilib.ai/kg/mathlib#Set.image2_vsub

English

image2 (· -ᵥ ·) s t = s -ᵥ t

Русский

image2 (· -ᵥ ·) s t = s -ᵥ t

LaTeX

$$$ \\mathrm{image2} (\\,\\cdot -ᵥ \\cdot\\,) s t = s -ᵥ t $$$

Lean4

@[simp]
theorem image2_vsub : image2 (· -ᵥ ·) s t = s -ᵥ t :=
  rfl

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

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

Разделы

Аффилиация

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