coe_toContinuousLinearEquivOfDetNeZero

English

If finrank 𝕜 E = finrank 𝕜 F for finite-dimensional topological vector spaces over a complete normed field 𝕜, then there exists a continuous linear equivalence E ≃L[𝕜] F.

Русский

Если для двух конечномерных топологических векторных пространств над полем 𝕜 выполнено finrank 𝕜 E = finrank 𝕜 F, то существует непрерывно линейное эквивалентное отображение E ≃L[𝕜] F.

LaTeX

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

Lean4

@[simp]
theorem coe_toContinuousLinearEquivOfDetNeZero (f : E →L[𝕜] E) (hf : f.det ≠ 0) :
    (f.toContinuousLinearEquivOfDetNeZero hf : E →L[𝕜] E) = f :=
  by
  ext x
  rfl

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