𝕜 : Type u_1
E : Type ?u.531909
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑(starRingEnd 𝕜) 0 * inner 0 x = 0
𝕜 : Type u_1
E : Type ?u.531909
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ inner 0 x = 0
rw [← zero_smul 𝕜 (0 : F), inner_smul_left]
no goals
𝕜 : Type u_1
E : Type ?u.531909
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ ↑(starRingEnd 𝕜) 0 * inner 0 x = 0
simp only [MulZeroClass.zero_mul, RingHom.map_zero]