addGroupIsAddTorsor

Mathlib.Algebra.AddTorsor.Defs

URI: https://scilib.ai/kg/mathlib#addGroupIsAddTorsor

Lean4

/-- An `AddGroup G` is a torsor for itself. -/
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/12096): linter not ported yet
--@[nolint instance_priority]

instance addGroupIsAddTorsor (G : Type*) [AddGroup G] : AddTorsor G G
    where
  vsub := Sub.sub
  vsub_vadd' := sub_add_cancel
  vadd_vsub' := add_sub_cancel_right

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

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

Разделы

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

Аффилиация

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