Theorem QuadraticAlgebra.coe_norm_eq_mul_star

Modification history

2025-12-16 09:36

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

chore: remove QuadraticAlgebra.coe (#32797) …

Deleted QuadraticAlgebra.coe_norm_eq_mul_star View on Github →

2025-11-01 12:56

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

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

Added QuadraticAlgebra.coe_norm_eq_mul_star View on Github →