𝕜 : Type u_1
E : Type ?u.538902
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
⊢ inner 0 0 = 0
𝕜 : Type u_1
E : Type ?u.538902
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x : F
⊢ x = 0 → inner x x = 0
rintro rfl
no goals
𝕜 : Type u_1
E : Type ?u.538902
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
⊢ inner 0 0 = 0
exact inner_zero_left _