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

split off deprecation

405e37b
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Aug 20, 2026 in 1m 26s