isometryOfInner_toLinearMap — Mathlib

English

The isometry produced from an inner-product-preserving linear equivalence is the same as that equivalence when viewed as a linear equivalence.

Русский

Изометрия, полученная из линейной эквивалентности, сохраняющей скалярное произведение, совпадает с этой эквивалентностью при рассмотрении как линейной эквивалентности.

LaTeX

$$$ (f : E \\simeq_{\,𝕜} E') \\toLinearEquiv = f $$$

Lean4

@[simp]
theorem isometryOfInner_toLinearMap (f : E →ₗ[𝕜] E') (h) : (f.isometryOfInner h).toLinearMap = f :=
  rfl

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