S : Type ?u.480390
R : Type u_1
R₁ : Type ?u.480396
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
hB : Anisotropic Q
x : M
hx : ∀ (n : M), bilin (↑associated' Q) x n = 0
⊢ ↑Q x = bilin (↑associated' Q) x x
S : Type ?u.480390
R : Type u_1
R₁ : Type ?u.480396
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
hB : Anisotropic Q
x : M
hx : ∀ (n : M), bilin (↑associated' Q) x n = 0
⊢ ↑Q x = 0
rw [← hx x]
no goals
S : Type ?u.480390
R : Type u_1
R₁ : Type ?u.480396
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Invertible 2
Q : QuadraticForm R M
hB : Anisotropic Q
x : M
hx : ∀ (n : M), bilin (↑associated' Q) x n = 0
⊢ ↑Q x = bilin (↑associated' Q) x x
exact (associated_eq_self_apply _ _ x).symm