maximalIdeal_mk

Mathlib.NumberTheory.NumberField.FinitePlaces

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

English

Reversing mk by maximalIdeal yields the original v: maximalIdeal (mk v) = v for a finite place v.

Русский

Возвращая v через maximalIdeal после mk, получаем исходное v: maximalIdeal (mk v) = v.

LaTeX

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

Lean4

theorem maximalIdeal_mk (v : HeightOneSpectrum (𝓞 K)) : maximalIdeal (mk v) = v := by rw [← mk_eq_iff, mk_maximalIdeal]

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

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

Разделы

Аффилиация

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