distrib

Mathlib.GroupTheory.FreeAbelianGroup

URI: https://scilib.ai/kg/mathlib#FreeAbelianGroup.distrib

Lean4

instance distrib : Distrib (FreeAbelianGroup α) :=
  { FreeAbelianGroup.mul α,
    FreeAbelianGroup.addCommGroup
      α with
    left_distrib := fun _ _ _ ↦ (lift _).map_add _ _
    right_distrib x y z := by simp [mul_def, ← Pi.add_def] }

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

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

Разделы

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

Аффилиация

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