isLocalRing — Mathlib

English

A valuation ring is a local ring.

Русский

Валюационное кольцо является локальным кольцом.

LaTeX

$$$\\text{IsLocalRing } A$$$

Lean4

instance (priority := 100) isLocalRing : IsLocalRing A :=
  IsLocalRing.of_isUnit_or_isUnit_one_sub_self
    (by
      intro a
      obtain ⟨c, h | h⟩ := PreValuationRing.cond a (1 - a)
      · left
        apply isUnit_of_mul_eq_one _ (c + 1)
        simp [mul_add, h]
      · right
        apply isUnit_of_mul_eq_one _ (c + 1)
        simp [mul_add, h])

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