mapGen

Mathlib.GroupTheory.Congruence.Hom

URI: https://scilib.ai/kg/mathlib#Con.mapGen

Lean4

/-- Given a function `f`, the smallest congruence relation containing the binary relation on `f`'s
image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the elements of `f⁻¹(y)`
by a congruence relation `c`.' -/
@[to_additive /-- Given a function `f`, the smallest additive congruence relation containing the
    binary relation on `f`'s image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to the
    elements of `f⁻¹(y)` by an additive congruence relation `c`.' -/
    ]
def mapGen {c : Con M} (f : M → N) : Con N :=
  conGen <| Relation.Map c f f

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

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

Разделы

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

Аффилиация

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