no goals
S : Type ?u.617859
R : Type ?u.617862
R₁ : Type u_1
M : Type ?u.617868
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₁)
f : (n → R₁) →ₗ[R₁] n → R₁
⊢ discr (comp Q f) = det (↑LinearMap.toMatrix' f) * det (↑LinearMap.toMatrix' f) * discr Q
simp only [Matrix.det_transpose, mul_left_comm, QuadraticForm.toMatrix'_comp, mul_comm,
  Matrix.det_mul, discr]