Theorem QuadraticAlgebra.omega_im

Modification history

2026-08-13 09:59

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

feat(Algebra/QuadraticAlgebra): discriminant and field criterion (#42206) …

Deleted QuadraticAlgebra.omega_im 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.omega_im View on Github →