integralBasis_apply — Mathlib

English

The i-th element of the integral basis is the image under the algebra map of the i-th element of RingOfIntegers.basis K.

Русский

i‑й элемент интегрального базиса равен образу i‑го элемента базиса кольца целых через алгебраическую карту.

LaTeX

$$$(integralBasis\\,K)\\,i = \\text{algebraMap} (\\mathcal{O}_K \\to K) (\\text{RingOfIntegers.basis } K\\,i).$$$

Lean4

@[simp]
theorem integralBasis_apply (i : Free.ChooseBasisIndex ℤ (𝓞 K)) :
    integralBasis K i = algebraMap (𝓞 K) K (RingOfIntegers.basis K i) :=
  Basis.localizationLocalization_apply ℚ (nonZeroDivisors ℤ) K (RingOfIntegers.basis K) i

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