inner_map_eq_flip — Mathlib

English

For a linear isometric equivalence f: E ≃ₗᵢ[𝕜] E' and x ∈ E, y ∈ E', we have ⟪f x, y⟫ = ⟪x, f^{-1} y⟫.

Русский

Для линейной изометрической эквиваленции f: E ≃ₗᵢ[𝕜] E' и элементов x ∈ E, y ∈ E' выполняется ⟪f x, y⟫ = ⟪x, f^{-1} y⟫.

LaTeX

$$$ \\forall x \\in E, \\forall y \\in E': \\langle f x, y \\rangle_𝕜 = \\langle x, f^{-1} y \\rangle_𝕜 $$$

Lean4

/-- The adjoint of a linear isometric equivalence is its inverse. -/
theorem inner_map_eq_flip (f : E ≃ₗᵢ[𝕜] E') (x : E) (y : E') : ⟪f x, y⟫_𝕜 = ⟪x, f.symm y⟫_𝕜 := by
  conv_lhs => rw [← f.apply_symm_apply y, f.inner_map_map]

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