piLp_equiv_toEuclideanCLM — Mathlib

English

The piLp-equivalence intertwines with the Euclidean CLM identification: the equiv respects the action of A on x.

Русский

Эквиверентность piLp согласуется с идентификацией через Euclidean CLM: эквив хорошо сохраняет действие A на x.

LaTeX

$$$WithLp.equiv _ _ (toEuclideanCLM A x) = A *ᵥ (WithLp.equiv _ _ x)$$$

Lean4

@[deprecated ofLp_toEuclideanCLM (since := "2025-05-07")]
theorem piLp_equiv_toEuclideanCLM (A : Matrix n n 𝕜) (x : EuclideanSpace 𝕜 n) :
    WithLp.equiv _ _ (toEuclideanCLM (n := n) (𝕜 := 𝕜) A x) = A *ᵥ (WithLp.equiv _ _ x) :=
  rfl

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