Theorem QuadraticAlgebra.norm_eq_zero_iff_eq_zero

Modification history

2026-05-01 23:00
Mathlib/Algebra/QuadraticAlgebra/Basic.lean
refactor(Algebra/QuadraticAlgebra): crush `ℚ`-algebra diamond (#38818) …
Modified QuadraticAlgebra.norm_eq_zero_iff_eq_zeroView 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_eq_zero_iff_eq_zeroView on Github →