subsingletonEquivFreeCommRing

Mathlib.RingTheory.FreeCommRing

URI: https://scilib.ai/kg/mathlib#FreeRing.subsingletonEquivFreeCommRing

Lean4

/-- If α has size at most 1 then the natural map from the free ring on `α` to the
free commutative ring on `α` is an isomorphism of rings. -/
def subsingletonEquivFreeCommRing [Subsingleton α] : FreeRing α ≃+* FreeCommRing α :=
  RingEquiv.ofBijective (coeRingHom _)
    (by
      have :
        (coeRingHom _ : FreeRing α → FreeCommRing α) =
          Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α) :=
        coe_eq α
      rw [this]
      apply Equiv.bijective)

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

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

Разделы

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

Аффилиация

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