English
Let R be a commutative semiring and n be a finite set. The map that sends a vector v ∈ R^n to the linear functional on R^n defined by t ↦ ⟨t, v⟩ (i.e., the dot product with v) is a linear equivalence between R^n and its R-dual.
Русский
Пусть R — коммутативное полупр."; пусть n — конечное множество. Отображение v ∈ R^n в линейный функционал на R^n, заданный t ↦ ⟨t, v⟩ (скалярное произведение с v), образует линейное взаимодополнение между R^n и его дуальной по отношению к R.
LaTeX
$$$$(n \to R) \;\cong_{R}\; (n \to R)^{*},\quad v \mapsto (t \mapsto \langle t, v\rangle).$$$$
Lean4
/-- The dot product as a linear equivalence to the dual. -/
@[simps]
def dotProductEquiv (R n : Type*) [CommSemiring R] [Fintype n] [DecidableEq n] : (n → R) ≃ₗ[R] Module.Dual R (n → R)
where
toFun v := ⟨⟨dotProduct v, dotProduct_add v⟩, fun t ↦ dotProduct_smul t v⟩
map_add' v w := by ext; simp
map_smul' t v := by ext; simp
invFun f i := f (LinearMap.single R _ i 1)
left_inv v := by simp
right_inv f := by ext; simp
