Revision #3136 → #3638 · back to history
modifiedGeneralized hypergeometric seriesb172bff54c34
| Field | From #3136 | To #3638 |
|---|
| note | Mathlib only has the ₂F₁ case (`ordinaryHypergeometricSeries`); the general pFq series is not formalized. | Mathlib has only the ₂F₁ case (`ordinaryHypergeometricSeries`); the general pFq series is not formalized. |
modifiedPower seriesdadf769c761b
| Field | From #3136 | To #3638 |
|---|
| note | Formal power series are represented by `FormalMultilinearSeries` (defined in `Mathlib.Analysis.Calculus.FormalMultilinearSeries`). | Formal power series are represented by `FormalMultilinearSeries`. |
modifiedRatio test for radius of convergencec6d6a3b00104
| Field | From #3136 | To #3638 |
|---|
| note | The ratio test for series convergence is available in Mathlib as `summable_of_ratio_test_tendsto_lt_one`. | The ratio test for series convergence is available as `summable_of_ratio_test_tendsto_lt_one`. |
modifiedRotation group SO(3)64d26a7889a1
| Field | From #3136 | To #3638 |
|---|
| note | `Matrix.specialOrthogonalGroup` (defined in `Mathlib.LinearAlgebra.UnitaryGroup`) is the special orthogonal group; SO(3) is the `Fin 3` instance. | `Matrix.specialOrthogonalGroup` is the special orthogonal group; SO(3) is the `Fin 3` instance. |
modifiedMeromorphic function0c95d51620f5
| Field | From #3136 | To #3638 |
|---|
| note | Meromorphic functions are formalized as `MeromorphicAt`/`MeromorphicOn` in Mathlib. | Meromorphic functions are formalized as `MeromorphicAt`/`MeromorphicOn`. |
addedRational functionf73805191d61
addedEntire function418af24f7c9e
addedLie groupa72f6ce4a6f6
addedElliptic function438c16aa06fd
addedRiemannian symmetric spacec3fe2230c5e6