reindex_smul

Mathlib.LinearAlgebra.AffineSpace.Basis

URI: https://scilib.ai/kg/mathlib#AffineBasis.reindex_smul

English

As above, smul and reindex commute: (a • b).reindex e = a • (b.reindex e).

Русский

Как указано выше, смул и переиндексация сохраняют взаимоотношения: (a • b).reindex e = a • (b.reindex e).

LaTeX

$$$ (a \\cdot b).reindex e = a \\cdot (b.reindex e)$$$

Lean4

@[simp]
theorem reindex_smul (a : G) (b : AffineBasis ι k V) (e : ι ≃ ι') : (a • b).reindex e = a • b.reindex e :=
  rfl

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

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

Разделы

Аффилиация

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