mk_apply — Mathlib

English

The operation mk on a finite place v and an element x is equal to the real absolute value of the embedding of x at v; mk v x = |embedding v x|.

Русский

Операция mk на конечном месте v и элементе x равна модулю отображения embed-ding v x: mk v x = |embedding v x|.

LaTeX

$$$\\mathrm{mk}\\,v\\,x = \\|\\mathrm{embedding}_v x\\|$$$

Lean4

@[simp]
theorem mk_apply (v : HeightOneSpectrum (𝓞 K)) (x : K) : mk v x = ‖embedding v x‖ :=
  rfl

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