maximalIdeal_injective — Mathlib

English

The map sending a finite place w to its maximal ideal is injective; distinct finite places have distinct maximal ideals.

Русский

Отображение w ↦ maximalIdeal w инъективно; разные конечные места задают разные максимальные идеалы.

LaTeX

$$((\\lambda w: maximalIdeal w).Injective)$$

Lean4

theorem maximalIdeal_injective : (fun w : FinitePlace K ↦ maximalIdeal w).Injective :=
  equivHeightOneSpectrum.injective

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