Theorem: ContinuousLinearMap.apply_eq_zero_of_eq_zero (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜✝ : Type
inst✝⁷ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝⁶ : Semiring R
𝕜 X Y : Type
inst✝⁵ : NormedField 𝕜
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup X
inst✝² : Module 𝕜 X
inst✝¹ : NormedAddCommGroup Y
inst✝ : Module 𝕜 Y
f : X →L[𝕜] Y
x : X
h : x = 0
⊢ f x = 0
Tactic:
rw [h, ContinuousLinearMap.map_zero]
State after:
no goals