norm_embedding_eq — Mathlib

English

For a finite place w and x ∈ K, the norm of embedding at maximalIdeal w applied to x equals w x; i.e., ||embedding (maximalIdeal w) x|| = w x.

Русский

Для конечного места w и элемента x ∈ K нормa вложения embedding при maximalIdeal w на x равна w x; то есть ||embedding (maximalIdeal w) x|| = w x.

LaTeX

$$$\\| \\mathrm{embedding}(\\mathrm{maximalIdeal}\,w)\\, x \\| = w\\,x$$$

Lean4

@[simp]
theorem norm_embedding_eq (w : FinitePlace K) (x : K) : ‖embedding (maximalIdeal w) x‖ = w x := by
  conv_rhs => rw [← mk_maximalIdeal w, mk_apply]

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