one

Mathlib.GroupTheory.Congruence.Defs

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

Lean4

@[to_additive]
instance one [MulOneClass M] (c : Con M) : One c.Quotient where
  -- Using Quotient.mk'' here instead of c.toQuotient
    -- since c.toQuotient is not reducible.
    -- This would lead to non-defeq diamonds since this instance ends up in
    -- quotients modulo ideals.
  one :=
    Quotient.mk''
      (1 : M)
        -- one := ((1 : M) : c.Quotient)

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

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

Разделы

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

Аффилиация

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