mk'

Mathlib.GroupTheory.Congruence.Hom

URI: https://scilib.ai/kg/mathlib#Con.mk'

Lean4

/-- The natural homomorphism from a monoid to its quotient by a congruence relation. -/
@[to_additive /-- The natural homomorphism from an `AddMonoid` to its quotient by an additive
    congruence relation. -/
    ]
def mk' : M →* c.Quotient where
  __ := mkMulHom c
  map_one' := rfl

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

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

Разделы

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

Аффилиация

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