Revision #2543 → #3162 · back to history
modifiedPolynomial GCD in simplifierd1719c4d0b1e
| Field | From #2543 | To #3162 |
|---|
| mathlib.module | Mathlib.Algebra.Polynomial.FieldDivision | Mathlib.Algebra.EuclideanDomain.Defs |
| note | Polynomial GCD is defined in Mathlib via EuclideanDomain/Polynomial.gcd, though it is not used for fraction simplification. | Polynomial GCD is defined in Mathlib via EuclideanDomain.gcd (Polynomial over a field is a EuclideanDomain), though it is not used for fraction simplification. |
modifiedPolynomial factorizationf20f6ccd0441
| Field | From #2543 | To #3162 |
|---|
| mathlib.module | Mathlib.RingTheory.UniqueFactorizationDomain.Basic | Mathlib.RingTheory.UniqueFactorizationDomain.Defs |
modifiedGreatest common divisore4a77a0bc509
| Field | From #2543 | To #3162 |
|---|
| mathlib.module | Mathlib.RingTheory.EuclideanDomain | Mathlib.Algebra.EuclideanDomain.Defs |
modifiedDerivatives of elementary and special functions1ad4de700964
| Field | From #2543 | To #3162 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.Deriv.Basic | Mathlib.Algebra.Polynomial.Derivative |
modifiedQuantifier elimination over reals19214c997456
| Field | From #2543 | To #3162 |
|---|
| mathlib.decl | FirstOrder.Language.Presburger | FirstOrder.Language.presburger |
| note | Mathlib has Presburger arithmetic quantifier elimination but not the Tarski–Seidenberg theorem for real-closed fields via CAD. | Mathlib defines the language of Presburger arithmetic but not the Tarski–Seidenberg theorem for real-closed fields via CAD. |
addedMultivariable polynomialsfaa45ca36e03
addedSpecial functions (Γ, ζ, erf, Bessel)e7371444fc39
addedAlgebraic numbers134fab6cd169
addedRational numbers (exact)2caca8cce0ee