toDual_toDual — Mathlib

English

The composition of the dual basis map with the basis map equals the evaluation at R on M, i.e., b.dualBasis.toDual ∘ b.toDual = Dual.eval R M.

Русский

Состав отображений dualBasis к toDual дает вычисление полю на M: b.dualBasis.toDual ∘ b.toDual = Dual.eval R M.

LaTeX

$$$ b.dualBasis.toDual \circ b.toDual = \operatorname{Dual.eval}_{R,M}. $$$

Lean4

@[simp]
theorem toDual_toDual : b.dualBasis.toDual.comp b.toDual = Dual.eval R M :=
  by
  refine b.ext fun i => b.dualBasis.ext fun j => ?_
  rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis, Dual.eval_apply, Basis.repr_self,
    Finsupp.single_apply, dualBasis_apply_self]

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