commMonoid

Mathlib.Algebra.GradedMonoid

URI: https://scilib.ai/kg/mathlib#GradedMonoid.GradeZero.commMonoid

Lean4

/-- The `CommMonoid` structure derived from `GCommMonoid A`. -/
instance commMonoid : CommMonoid (A 0) :=
  Function.Injective.commMonoid (mk 0) sigma_mk_injective rfl mk_zero_smul mk_zero_pow

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

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

Разделы

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

Аффилиация

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