Theorem: ContinuousMultilinearMap.toFun_eq_coe (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝⁸ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝⁷ : Semiring R✝
R A B : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
f : ContinuousMultilinearMap R (fun x => A) B
⊢ f.toFun = ⇑f
Tactic:
rw [MultilinearMap.toFun_eq_coe]
State after:
n : ℕ
𝕜 : Type
inst✝⁸ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝⁷ : Semiring R✝
R A B : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
f : ContinuousMultilinearMap R (fun x => A) B
⊢ ⇑f.toMultilinearMap = ⇑f

State before:
n : ℕ
𝕜 : Type
inst✝⁸ : NontriviallyNormedField 𝕜
R✝ A✝ B✝ E : Type
inst✝⁷ : Semiring R✝
R A B : Type
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : TopologicalSpace B
f : ContinuousMultilinearMap R (fun x => A) B
⊢ ⇑f.toMultilinearMap = ⇑f
Tactic:
simp
State after:
no goals