basis_apply_eq_mkQ

Mathlib.LinearAlgebra.FreeModule.ModN

URI: https://scilib.ai/kg/mathlib#ModN.basis_apply_eq_mkQ

English

The basis map coincides with the mkQ map on indices, i.e., basis b evaluated at i equals mkQ n applied to b i.

Русский

База на позиции i совпадает: b i = mkQ n (b i).

LaTeX

$$basis b i = mkQ n (b i)$$

Lean4

theorem basis_apply_eq_mkQ {ι : Type*} (b : Basis ι ℤ G) (i : ι) : basis b i = mkQ n (b i) := by
  rw [Basis.apply_eq_iff]; simp [basis, mkQ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru