toLin_finTwoProd_toContinuousLinearMap

English

Given finrank 𝕜 E = finrank 𝕜 F, there is a continuous linear equivalence E ≃L[𝕜] F constructed by a finite-dimensional isomorphism.

Русский

Пусть выполнено равенство конечной размерности; существует построимое непрерывно линейное эквивалентное отображение E ≃L[𝕜] F.

LaTeX

$$$\\operatorname{finrank}_{𝕜} E = \\operatorname{finrank}_{𝕜} F \\Rightarrow E \\simeq_L[𝕜] F$$$

Lean4

theorem _root_.Matrix.toLin_finTwoProd_toContinuousLinearMap (a b c d : 𝕜) :
    LinearMap.toContinuousLinearMap (Matrix.toLin (Basis.finTwoProd 𝕜) (Basis.finTwoProd 𝕜) !![a, b; c, d]) =
      (a • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + b • ContinuousLinearMap.snd 𝕜 𝕜 𝕜).prod
        (c • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + d • ContinuousLinearMap.snd 𝕜 𝕜 𝕜) :=
  ContinuousLinearMap.ext <| Matrix.toLin_finTwoProd_apply _ _ _ _

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