Theorem: ContinuousMultilinearMap.norm_empty (ForML/ContinuousMultilinearMap.lean)

State before:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖c x‖ = ‖c‖
Tactic:
rw [c.eq_empty]
State after:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E (c 0)) x‖ = ‖constOfIsEmpty 𝕜 E (c 0)‖

State before:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E (c 0)) x‖ = ‖constOfIsEmpty 𝕜 E (c 0)‖
Tactic:
rw [constOfIsEmpty_apply, norm_constOfIsEmpty]
State after:
no goals