dotProduct_comp_equiv_symm — Mathlib

English

Permuting a vector on the left of a dot product transfers to the right with an equivalence e: m ≃ n: u ∘ e^{-1} • dot with x equals u • dot with x ∘ e.

Русский

Перестановка индексов слева от скалярного произведения переносится вправо через эквивалентность: dotProduct(u ∘ e^{-1}, x) = dotProduct(u, x ∘ e).

LaTeX

$$$$ (u \circ e^{-1}) \; \boxed{\cdot} \; x = u \; \boxed{\cdot} \; (x \circ e). $$$$

Lean4

/-- Permuting a vector on the right of a dot product can be transferred to the left. -/
@[simp]
theorem dotProduct_comp_equiv_symm (e : n ≃ m) : u ⬝ᵥ x ∘ e.symm = u ∘ e ⬝ᵥ x := by
  simpa only [Equiv.symm_symm] using (comp_equiv_symm_dotProduct u x e.symm).symm

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