mk_maximalIdeal

Mathlib.NumberTheory.NumberField.FinitePlaces

URI: https://scilib.ai/kg/mathlib#NumberField.FinitePlace.mk_maximalIdeal

English

For a finite place w, mk (maximalIdeal w) returns back w; mk (maximalIdeal w) = w.

Русский

Для конечного места w отображение mk (maximalIdeal w) возвращает исходное w; mk (maximalIdeal w) = w.

LaTeX

$$$\\mathrm{mk}(\\mathrm{maximalIdeal}\,w) = w$$$

Lean4

@[simp]
theorem mk_maximalIdeal (w : FinitePlace K) : mk (maximalIdeal w) = w :=
  Subtype.ext w.2.choose_spec

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru