comp_equiv_dotProduct_comp_equiv — Mathlib

English

Symmetric transfer of index permutation on both sides of a dot product: dotProduct(u, x) = dotProduct(x, u) under equivalential relabeling.

Русский

Симметричный перенос перестановки индексов между двумя аргументами скалярного произведения.

LaTeX

$$$$ \operatorname{dotProduct}(u, x) = \operatorname{dotProduct}(x, u) $$$$

Lean4

/-- Permuting vectors on both sides of a dot product is a no-op. -/
@[simp]
theorem comp_equiv_dotProduct_comp_equiv (e : m ≃ n) : x ∘ e ⬝ᵥ y ∘ e = x ⬝ᵥ y := by
  simp [← dotProduct_comp_equiv_symm, Function.comp_def _ e.symm]

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