basis_apply

Mathlib.RingTheory.TensorProduct.Free

URI: https://scilib.ai/kg/mathlib#Algebra.TensorProduct.basis_apply

English

Compute the i-th basis element: it equals 1 ⊗ b_i.

Русский

Для i-й элемент базиса: равенство 1 ⊗ b_i.

LaTeX

$$$basis A b\, i = 1 ⊗ₜ b_i$$$

Lean4

@[simp]
theorem basis_apply (i : ι) : basis A b i = 1 ⊗ₜ b i :=
  basis_repr_symm_apply b 1 i

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

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

Разделы

Аффилиация

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