le_isUnit_iff_zero_notMem — Mathlib

English

In a local ring, a submonoid M is contained in the units iff 0 is not in M.

Русский

В локальном кольце подмонойд M содержится в единичных элементах тогда и только если 0 не принадлежит M.

LaTeX

$$[IsLocalRing R] ⇒ (M ≤ IsUnit.submonoid R ⇔ 0 ∉ M)$$

Lean4

@[simp]
theorem le_isUnit_iff_zero_notMem [IsLocalRing R] {M : Submonoid R} : M ≤ IsUnit.submonoid R ↔ 0 ∉ M :=
  by
  have := ((Ring.krullDimLE_zero_and_isLocalRing_tfae R).out 0 2 rfl rfl).mp ⟨‹_›, ‹_›⟩
  exact ⟨fun h₁ h₂ ↦ not_isUnit_zero (h₁ h₂), fun H x hx ↦ (this x).not_left.mp fun ⟨n, hn⟩ ↦ H (hn ▸ pow_mem hx n)⟩

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