gi

Mathlib.GroupTheory.Congruence.Defs

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

Lean4

/-- There is a Galois insertion of congruence relations on a type with a multiplication `M` into
binary relations on `M`. -/
@[to_additive /-- There is a Galois insertion of additive congruence relations on a type with
    an addition `M` into binary relations on `M`. -/
    ]
protected def gi : @GaloisInsertion (M → M → Prop) (Con M) _ _ conGen DFunLike.coe
    where
  choice r _ := conGen r
  gc _ c := ⟨fun H _ _ h => H <| ConGen.Rel.of _ _ h, @fun H => conGen_of_con c ▸ conGen_mono H⟩
  le_l_u x := (conGen_of_con x).symm ▸ le_refl x
  choice_eq _ _ := rfl

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

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

Разделы

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

Аффилиация

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