ofZLatticeBasis_apply — Mathlib

English

For each index i, the i-th vector of the constructed K-basis obtained from the ℤ-basis b equals the i-th vector of b.

Русский

Для каждого индекса i i-й вектор построенной K-базы, полученной из ℤ-базы b, равен i-му вектору b.

LaTeX

$$$(b\\text{.ofZLatticeBasis } K L).i = b_i \\quad (\\forall i)$$$

Lean4

@[simp]
theorem ofZLatticeBasis_apply (i : ι) : b.ofZLatticeBasis K L i = b i := by simp [Basis.ofZLatticeBasis]

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