dualDistribInvOfBasis_apply — Mathlib

English

The equality expressing the explicit expansion of dualDistribInvOfBasis: it equals the finite double sum of f evaluated at basis tensors times the corresponding dual basis tensors.

Русский

Выражение для двойного распределения через базисы: равенство, что dualDistribInvOfBasis равно конечной двойной сумме f(b_i ⊗ c_j) × b_i^* ⊗ c_j^*.

LaTeX

$$$$ dualDistribInvOfBasis b c f = \\sum_i \\sum_j f(b_i \\otimes c_j) \\; b_i^* \\otimes c_j^*. $$$$

Lean4

@[simp]
theorem dualDistribInvOfBasis_apply (b : Basis ι R M) (c : Basis κ R N) (f : Dual R (M ⊗[R] N)) :
    dualDistribInvOfBasis b c f = ∑ i, ∑ j, f (b i ⊗ₜ c j) • b.dualBasis i ⊗ₜ c.dualBasis j := by
  simp [dualDistribInvOfBasis]

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