coe_norm_int — Mathlib

English

For x in the ring of integers 𝓞 K, the integer-norm agrees with the field-norm after embedding into K: the integer norm mapped to Q equals the K-norm of x.

Русский

Для x из кольца целых чисел 𝓞 K нормa по целым числам совмещается с полевой нормой после вложения в K: нормa по Z сопоставляет норму по Q полевой норме на x.

LaTeX

$$$ (\mathsf{norm}_{\mathbb{Z}}(x))_{\mathbb{Q}} = \mathsf{norm}_{\mathbb{Q}}(x) \qquad (x \in \mathscr{O}K) $$$

Lean4

theorem coe_norm_int : (Algebra.norm ℤ x : ℚ) = Algebra.norm ℚ (x : K) :=
  (Algebra.norm_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm

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