instAddCommGroup

Mathlib.Topology.Algebra.GroupCompletion

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

Lean4

instance instAddCommGroup : AddCommGroup (Completion α) :=
  { (inferInstance : AddGroup <| Completion α) with
    add_comm := fun a b ↦
      Completion.induction_on₂ a b
        (isClosed_eq (continuous_map₂ continuous_fst continuous_snd) (continuous_map₂ continuous_snd continuous_fst))
        fun x y ↦ by
        change (x : Completion α) + ↑y = ↑y + ↑x
        rw [← coe_add, ← coe_add, add_comm] }

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

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

Разделы

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

Аффилиация

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