Theorem QuadraticAlgebra.norm_intCast

Modification history

2025-11-24 20:05

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

chore: tidy various files (#31907)

Modified QuadraticAlgebra.norm_intCast 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.norm_intCast View on Github →