coe_trace_int — Mathlib

English

For x in 𝓞 K, the integer-trace equals the field-trace after embedding into K: Tr_Z(x) in Q equals Tr_Q(x).

Русский

Для x из 𝓞 K след по целым числам равен полевой следу после вложения в K: Tr_Z(x) ∈ Q = Tr_Q(x).

LaTeX

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

Lean4

theorem coe_trace_int : (Algebra.trace ℤ _ x : ℚ) = Algebra.trace ℚ K (x : K) :=
  (Algebra.trace_localization (R := ℤ) (Rₘ := ℚ) (S := 𝓞 K) (Sₘ := K) (nonZeroDivisors ℤ) x).symm

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