Theorem Algebra.leftMulMatrix_quadraticAlgebra

Modification history

2026-10-17 12:17
Mathlib/RingTheory/QuadraticAlgebra.lean
feat(RingTheory/QuadraticAlgebra): trace, norm and discriminant as `Algebra` invariants (#42297) …
Added Algebra.leftMulMatrix_quadraticAlgebraView on Github →