Revision #3191 → #3689 · back to history
modifiedAffine geometry0b991f720464
| Field | From #3191 | To #3689 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.AffineSpace.Defs | Mathlib.Algebra.Torsor.Defs |
| note | `AffineSpace` (notation for `AddTorsor`) formalizes the central object, not the informal disciplinary definition. | `AffineSpace` (notation for `AddTorsor`, now in `Mathlib.Algebra.Torsor.Defs`) formalizes the central object, not the informal disciplinary definition. |
modifiedCyclic group of order two0e2491407950
| Field | From #3191 | To #3689 |
|---|
| mathlib.module | Mathlib.Data.ZMod.Basic | Mathlib.Data.ZMod.Defs |
modifiedSine and cosine (power series)b43e7adba539
| Field | From #3191 | To #3689 |
|---|
| kind | theorem | definition |
| label | Infinite series for π/trigonometric functions (Indian mathematics) | Sine and cosine (power series) |
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | Mathlib.Analysis.Complex.Trigonometric |
modifiedHomological algebra7785182993f2
| Field | From #3191 | To #3689 |
|---|
| mathlib.decl | CategoryTheory.ShortComplex.HomologicalComplex | HomologicalComplex |
| note | Chain complexes and homology are formalized in `Mathlib.Algebra.Homology`; the discipline as a whole is not a single object. | Chain complexes and homology are formalized in `Mathlib.Algebra.Homology` (e.g. `HomologicalComplex`); the discipline as a whole is not a single object. |
addedNatural numbersfc04d12bf4b0
addedIntegers5903f7302641
addedRational numbersc4bcc85d84f5
addedPrime numbers9130d3ea120e
addedAnalytic number theoryabc901761f07
addedAlgebraic number theory6cfbe8dbc7de
addedReal numbers705dc2ca6e19
addedComplex numbers5e9f50799f68
addedPartial differential equations769495798c2d
addedFractal / self-similarity7d182c7982a5
addedModel theoryccc1a7129461
addedInteger factorization problem23f71b6185c6