op

Mathlib.GroupTheory.Congruence.Opposite

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

Lean4

/-- If `c` is a multiplicative congruence on `M`, then `(a, b) ↦ c b.unop a.unop` is a
multiplicative congruence on `Mᵐᵒᵖ`. -/
@[to_additive /-- If `c` is an additive congruence on `M`, then `(a, b) ↦ c b.unop a.unop` is an
    additive congruence on `Mᵃᵒᵖ` -/
    ]
def op (c : Con M) : Con Mᵐᵒᵖ where
  r a b := c b.unop a.unop
  iseqv :=
    { refl := fun a ↦ c.refl a.unop
      symm := c.symm
      trans := fun h1 h2 ↦ c.trans h2 h1 }
  mul' h1 h2 := c.mul h2 h1

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

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

Разделы

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

Аффилиация

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