instAddTorsor

Mathlib.Algebra.AddTorsor.Basic

URI: https://scilib.ai/kg/mathlib#Pi.instAddTorsor

Lean4

/-- A product of `AddTorsor`s is an `AddTorsor`. -/
instance instAddTorsor : AddTorsor (∀ i, fg i) (∀ i, fp i)
    where
  vsub p₁ p₂ i := p₁ i -ᵥ p₂ i
  vsub_vadd' p₁ p₂ := funext fun i => vsub_vadd (p₁ i) (p₂ i)
  vadd_vsub' g p := funext fun i => vadd_vsub (g i) (p i)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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