isometryOfInner_toLinearEquiv — Mathlib

English

The adjoint of a linear isometric equivalence is its inverse, i.e., ⟪f x, y⟫ = ⟪x, f.symm y⟫.

Русский

Сопряжённая линейной изометрической эквивалентности есть её обратная, т.е. ⟪f x, y⟫ = ⟪x, f.symm y⟫.

LaTeX

$$$ \\langle f x, y \\rangle_𝕜 = \\langle x, f^{-1} y \\rangle_𝕜 $$$

Lean4

@[simp]
theorem isometryOfInner_toLinearEquiv (f : E ≃ₗ[𝕜] E') (h) : (f.isometryOfInner h).toLinearEquiv = f :=
  rfl

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