addGroup

Mathlib.Topology.Algebra.GroupCompletion

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.addGroup

Lean4

instance addGroup : AddGroup (Completion α) :=
  { (inferInstance : SubNegMonoid <| Completion α) with
    neg_add_cancel := fun a ↦
      Completion.induction_on a (isClosed_eq (continuous_map₂ Completion.continuous_map continuous_id) continuous_const)
        fun a ↦
        show -(a : Completion α) + a = 0 by
          rw_mod_cast [neg_add_cancel]
          rfl }

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

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

Разделы

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

Аффилиация

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