Skip to content

[Merged by Bors] - chore(Algebra/QuadraticAlgebra): rename Discr to Discriminant - #42975

Closed
xroblot wants to merge 2 commits into
leanprover-community:masterfrom
xroblot:rename-discr-file
Closed

[Merged by Bors] - chore(Algebra/QuadraticAlgebra): rename Discr to Discriminant#42975
xroblot wants to merge 2 commits into
leanprover-community:masterfrom
xroblot:rename-discr-file

Commits

Commits on Aug 19, 2026

Commits on Aug 20, 2026