case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁸ : AddCommGroup E
inst✝¹⁷ : Module 𝕜 E
inst✝¹⁶ : TopologicalSpace E
inst✝¹⁵ : TopologicalAddGroup E
inst✝¹⁴ : ContinuousSMul 𝕜 E
F : Type w
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : TopologicalAddGroup F
inst✝⁹ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : E
⊢ ↑(toContinuousLinearEquiv e).toLinearEquiv x = ↑e x
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁸ : AddCommGroup E
inst✝¹⁷ : Module 𝕜 E
inst✝¹⁶ : TopologicalSpace E
inst✝¹⁵ : TopologicalAddGroup E
inst✝¹⁴ : ContinuousSMul 𝕜 E
F : Type w
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : TopologicalAddGroup F
inst✝⁹ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ (toContinuousLinearEquiv e).toLinearEquiv = e
ext x
no goals
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹⁸ : AddCommGroup E
inst✝¹⁷ : Module 𝕜 E
inst✝¹⁶ : TopologicalSpace E
inst✝¹⁵ : TopologicalAddGroup E
inst✝¹⁴ : ContinuousSMul 𝕜 E
F : Type w
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : TopologicalSpace F
inst✝¹⁰ : TopologicalAddGroup F
inst✝⁹ : ContinuousSMul 𝕜 F
F' : Type x
inst✝⁸ : AddCommGroup F'
inst✝⁷ : Module 𝕜 F'
inst✝⁶ : TopologicalSpace F'
inst✝⁵ : TopologicalAddGroup F'
inst✝⁴ : ContinuousSMul 𝕜 F'
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : E
⊢ ↑(toContinuousLinearEquiv e).toLinearEquiv x = ↑e x
rfl