case a.h
S : Type ?u.554283
R : Type ?u.554286
R₁ : Type u_1
M : Type ?u.554292
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R₁
inst✝² : AddCommMonoid M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
Q : QuadraticForm R₁ (n → R₁)
i j : n
⊢ Matrix.transpose (toMatrix' Q) i j = toMatrix' Q i j
S : Type ?u.554283
R : Type ?u.554286
R₁ : Type u_1
M : Type ?u.554292
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R₁
inst✝² : AddCommMonoid M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
Q : QuadraticForm R₁ (n → R₁)
⊢ Matrix.IsSymm (toMatrix' Q)
ext (i j)
no goals
case a.h
S : Type ?u.554283
R : Type ?u.554286
R₁ : Type u_1
M : Type ?u.554292
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R₁
inst✝² : AddCommMonoid M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
Q : QuadraticForm R₁ (n → R₁)
i j : n
⊢ Matrix.transpose (toMatrix' Q) i j = toMatrix' Q i j
rw [toMatrix', Matrix.transpose_apply, BilinForm.toMatrix'_apply, BilinForm.toMatrix'_apply,
  associated_isSymm]