Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-05-01 23:00
4b7e5c1b
View on Github →
refactor(Algebra/QuadraticAlgebra): crush
ℚ
-algebra diamond (
#38818
) From FormalConjectures
Estimated changes
Modified
Mathlib/Algebra/QuadraticAlgebra/Basic.lean
modified
theorem
QuadraticAlgebra.norm_eq_zero_iff_eq_zero
Modified
Mathlib/Algebra/QuadraticAlgebra/Defs.lean