nonUnitalNonAssocRing

Mathlib.GroupTheory.FreeAbelianGroup

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

Lean4

instance nonUnitalNonAssocRing : NonUnitalNonAssocRing (FreeAbelianGroup α) :=
  { FreeAbelianGroup.distrib,
    FreeAbelianGroup.addCommGroup
      _ with
    zero_mul := fun a ↦ by
      have h : 0 * a + 0 * a = 0 * a := by simp [← add_mul]
      simpa using h
    mul_zero := fun _ ↦ rfl }

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

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

Разделы

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

Аффилиация

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