notMem_maximalIdeal — Mathlib

English

In a local ring, an element is a unit if and only if it is not in the maximal ideal.

Русский

В локальном кольце элемент является единицей тогда и только тогда, когда он не принадлежит максимальному идеалу.

LaTeX

$$$ x \notin \mathfrak{m} \iff x \in R^{\times}. $$$

Lean4

/-- An element `x` of a commutative local semiring is not contained in the maximal ideal
iff it is a unit.
-/
theorem notMem_maximalIdeal {x : R} : x ∉ maximalIdeal R ↔ IsUnit x := by
  simp only [mem_maximalIdeal, mem_nonunits_iff, not_not]

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