basis_repr_symm_apply' — Mathlib

English

The symm version of the basis repr sends Finsupp singleton to tensor product form.

Русский

Симметризированная версия отображения базиса переводит единичный элемент Finsupp в тензорную форму.

LaTeX

$$$basis_repr_symm_apply' (a) (i) : a • basis A b i = a ⊗ₜ b i$$$

Lean4

theorem basis_repr_symm_apply' (a : A) (i : ι) : a • basis A b i = a ⊗ₜ b i := by
  simpa using basis_repr_symm_apply b a i

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