S : Type ?u.690539
R : Type u_1
R₁ : Type ?u.690545
M : Type u_2
M₁ : Type ?u.690551
inst✝⁶ : Semiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
ι : Type u_3
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticForm R M
w : ι → R
⊢ ↑(basisRepr Q v) w = ↑Q (↑(LinearEquiv.symm (Basis.equivFun v)) fun i => w i)
S : Type ?u.690539
R : Type u_1
R₁ : Type ?u.690545
M : Type u_2
M₁ : Type ?u.690551
inst✝⁶ : Semiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
ι : Type u_3
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticForm R M
w : ι → R
⊢ ↑(basisRepr Q v) w = ↑Q (∑ i : ι, w i • ↑v i)
rw [← v.equivFun_symm_apply]
no goals
S : Type ?u.690539
R : Type u_1
R₁ : Type ?u.690545
M : Type u_2
M₁ : Type ?u.690551
inst✝⁶ : Semiring R
inst✝⁵ : CommSemiring R₁
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
ι : Type u_3
inst✝ : Fintype ι
v : Basis ι R M
Q : QuadraticForm R M
w : ι → R
⊢ ↑(basisRepr Q v) w = ↑Q (↑(LinearEquiv.symm (Basis.equivFun v)) fun i => w i)
rfl