Theorem QuadraticAlgebra.zsmul_val

Modification history

2025-11-01 12:56

Mathlib/Algebra/QuadraticAlgebra.lean

feat(Mathlib/Algebra/QuadraticAlgebra): norm, star structure on quadratic alg. (#30059) …

Added QuadraticAlgebra.zsmul_val View on Github →