congr

Mathlib.GroupTheory.Congruence.Basic

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

Lean4

/-- Makes an isomorphism of quotients by two congruence relations, given that the relations are
equal. -/
@[to_additive /-- Makes an additive isomorphism of quotients by two additive congruence relations,
    given that the relations are equal. -/
    ]
protected def congr {c d : Con M} (h : c = d) : c.Quotient ≃* d.Quotient :=
  { Quotient.congr (Equiv.refl M) <| by apply Con.ext_iff.mp h with
    map_mul' := fun x y => by rcases x with ⟨⟩; rcases y with ⟨⟩; rfl }

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

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

Разделы

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

Аффилиация

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