toContinuousLinearMap₁_coe — Mathlib

English

If a linear equivalence e is a homothety with ratio a, then its inverse is a homothety with ratio a^{-1}.

Русский

Если линейное эквивалентное отображение является гомотетией с коэффициентом a, его обратное также гомотетично с коэффициентом a^{-1}.

LaTeX

$$$(\forall x)\|e x\| = a \|x\| \Rightarrow \|e^{-1} y\| = a^{-1} \|y\|$$$

Lean4

@[simp]
theorem toContinuousLinearMap₁_coe (f : 𝕜 →ₗ[𝕜] E) : (f.toContinuousLinearMap₁ : 𝕜 →ₗ[𝕜] E) = f :=
  rfl

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