gCommMonoid

Mathlib.Algebra.GradedMonoid

URI: https://scilib.ai/kg/mathlib#SetLike.gCommMonoid

Lean4

/-- Build a `GCommMonoid` instance for a collection of subobjects. -/
instance gCommMonoid {S : Type*} [SetLike S R] [CommMonoid R] [AddCommMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] :
    GradedMonoid.GCommMonoid fun i => A i :=
  { SetLike.gMonoid A with mul_comm := fun ⟨_, _, _⟩ ⟨_, _, _⟩ => Sigma.subtype_ext (add_comm _ _) (mul_comm _ _) }

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

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

Разделы

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

Аффилиация

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