quotientQuotientEquivQuotient

Mathlib.GroupTheory.Congruence.Basic

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

Lean4

/-- The **third isomorphism theorem for monoids**. -/
@[to_additive /-- The third isomorphism theorem for `AddMonoid`s. -/
    ]
def quotientQuotientEquivQuotient (c d : Con M) (h : c ≤ d) : (ker (c.map d h)).Quotient ≃* d.Quotient :=
  { Setoid.quotientQuotientEquivQuotient c.toSetoid d.toSetoid h with
    map_mul' := fun x y =>
      Con.induction_on₂ x y fun w z =>
        Con.induction_on₂ w z fun a b => show _ = d.mk' a * d.mk' b by rw [← d.mk'.map_mul]; rfl }

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

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

Разделы

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

Аффилиация

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