Revision #2477 → #3100 · back to history
modifiedGeometric series225334c4d19e
| Field | From #2477 | To #3100 |
|---|
| mathlib.module | Mathlib.Algebra.Field.GeomSum | Mathlib.Algebra.GeomSum |
modifiedGeometric series (finite/infinite)d80c8b0d9f39
| Field | From #2477 | To #3100 |
|---|
| mathlib.module | Mathlib.Algebra.Field.GeomSum | Mathlib.Algebra.GeomSum |
| provenance | ai | ai-moderated |
modifiedFinite geometric sum closed form708736c7b8f5
| Field | From #2477 | To #3100 |
|---|
| mathlib.module | Mathlib.Algebra.Field.GeomSum | Mathlib.Algebra.GeomSum |
| note | The finite closed form `∑ i ∈ range n, r^i = (r^n - 1)/(r - 1)` for `r ≠ 1` is `geom_sum_eq`; module corrected to `Mathlib.Algebra.Field.GeomSum`. | The finite closed form `∑ i ∈ range n, r^i = (r^n - 1)/(r - 1)` for `r ≠ 1` is `geom_sum_eq`. |
| provenance | ai | ai-moderated |
addedAbsolute value of ratio via norm49c09e2abc82