lift_residue_apply — Mathlib

English

An element x belongs to the maximal ideal if and only if its residue is zero.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lift_residue_apply {R S : Type*} [CommRing R] [IsLocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] (x) :
    lift f (residue R x) = f x :=
  rfl

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