residue_eq_zero_iff — Mathlib

English

An element x of R lies in the maximal ideal if and only if its residue is zero.

Русский

Элемент x ∈ R принадлежит максимальному идеалу тогда и только тогда, когда его остаток равен нулю.

LaTeX

$$$\\mathrm{residue}_R(x) = 0 \\iff x \\in \\mathfrak m_R$$$

Lean4

@[simp]
theorem residue_eq_zero_iff (x : R) : residue R x = 0 ↔ x ∈ maximalIdeal R := by rw [← RingHom.mem_ker, ker_residue]

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