integralBasis_repr_apply — Mathlib

English

The coordinates of the image of x under the integralBasis basis correspond to the rationals obtained from the RingOfIntegers basis representation.

Русский

Координаты изображения x через интегральный базис совпадают с рациональными координатами по базису RingOfIntegers.

LaTeX

$$$(integralBasis\\,K).repr(\\text{algebraMap}_{\\mathcal{O}_K\\to K}(x))\\,i = (\\text{algebraMap}_{\\mathbb{Z}\\to\\mathbb{Q}})( (RingOfIntegers.basis K).repr x\\,i).$$$

Lean4

@[simp]
theorem integralBasis_repr_apply (x : (𝓞 K)) (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
    (integralBasis K).repr (algebraMap _ _ x) i = (algebraMap ℤ ℚ) ((RingOfIntegers.basis K).repr x i) :=
  Basis.localizationLocalization_repr_algebraMap ℚ (nonZeroDivisors ℤ) K _ x i

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