instIsLocalRing

Mathlib.RingTheory.LocalRing.Basic

URI: https://scilib.ai/kg/mathlib#Field.instIsLocalRing

← MathLib Explorer

English

Every field K is a local ring.

Русский

Каждое поле K является локальным кольцом.

LaTeX

$$$K\\text{ field} \\Rightarrow IsLocalRing(K)$$$

Lean4

instance (priority := 100) : IsLocalRing K := by
  classical
    exact
    IsLocalRing.of_isUnit_or_isUnit_one_sub_self fun a =>
      if h : a = 0 then Or.inr (by rw [h, sub_zero]; exact isUnit_one) else Or.inl <| IsUnit.mk0 a h

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

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

Разделы

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

Аффилиация

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