no goals
S : Type ?u.614314
R : Type ?u.614317
R₁ : Type u_1
M : Type ?u.614323
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : CommRing R₁
inst✝³ : DecidableEq n
inst✝² : Invertible 2
m : Type w
inst✝¹ : DecidableEq m
inst✝ : Fintype m
Q : QuadraticForm R₁ (n → R₁)
a : R₁
⊢ discr (a • Q) = a ^ Fintype.card n * discr Q
simp only [discr, toMatrix'_smul, Matrix.det_smul]