Quadratic Algebra

We prove that the expression for the norm of an element in a quadratic algebra comes from looking at the endomorphism defined by left multiplication by that element and taking its determinant.

@[simp]

theorem QuadraticAlgebra.det_toLinearMap_eq_norm {R : Type u_1} [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) : LinearMap.det (DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z) = norm z

The norm of an element in a quadratic algebra is the determinant of the endomorphism defined by left multiplication by that element.