algebraMap_mem_maximalIdeal_iff — Mathlib

English

An element x of the base ring lies in the maximal ideal of the base valuation subring if and only if its image in the extension lies in the maximal ideal there.

Русский

Элемент x базового кольца лежит в максимальном идеале базового подкольца оценки тогда и только тогда, когда его образ в расширении лежит в максимальном идеале в расширении.

LaTeX

$$$\\ algebraMap_{K_0}^L (x) \\in \\mathfrak{m}_{L_0} \\;\\Longleftrightarrow \\; x \\in \\mathfrak{m}_{K_0}$$$

Lean4

theorem algebraMap_mem_maximalIdeal_iff {x : K₀} : algebraMap K₀ L₀ x ∈ (maximalIdeal L₀) ↔ x ∈ maximalIdeal K₀ := by
  simp [mem_maximalIdeal, map_mem_nonunits_iff, _root_.mem_nonunits_iff]

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