Theorems · Theorem · ring theory

QuadraticAlgebra.det_toLinearMap_eq_norm

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

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

Defined in

Mathlib.Algebra.QuadraticAlgebra.NormDeterminant

Cited by

0 results in Mathlib

Foundations

Depth 130 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing