Theorems · Theorem · functional analysis

LinearIsometry.coe_toLinearIsometryEquiv

∀ {F : Type u_1} {E₁ : Type u_2} [inst : SeminormedAddCommGroup F] [inst_1 : NormedAddCommGroup E₁] {R₁ : Type u_3}
  [inst_2 : Field R₁] [inst_3 : Module R₁ E₁] [inst_4 : Module R₁ F] [inst_5 : FiniteDimensional R₁ E₁]
  [inst_6 : FiniteDimensional R₁ F] (li : E₁ →ₗᵢ[R₁] F) (h : Module.finrank R₁ E₁ = Module.finrank R₁ F),
  ⇑(li.toLinearIsometryEquiv h) = ⇑li

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

0 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupNormedAddCommGroupFieldModuleModuleFiniteDimensionalFiniteDimensional