Revision #1263 → #2034 · back to history
modifiedLinear recurrence relation7e220fdca2d9
| Field | From #1263 | To #2034 |
|---|
| mathlib.module | Mathlib.Algebra.GroupPower.Basic | Mathlib.Algebra.Group.Defs |
modifiedSign behavior with positive ratiof1822b3aee90
| Field | From #1263 | To #2034 |
|---|
| mathlib.module | Mathlib.Algebra.Order.Ring.Lemmas | Mathlib.Algebra.Order.GroupWithZero.Basic |
modifiedConstant magnitude when |r| = 1be9597d782de
| Field | From #1263 | To #2034 |
|---|
| mathlib.module | Mathlib.Analysis.Normed.Field.Basic | Mathlib.Analysis.Normed.Ring.Basic |
modifiedCorrespondence with arithmetic sumc276c5e0dd7b
| Field | From #1263 | To #2034 |
|---|
| mathlib.decl | — | Finset.sum_range_id |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Algebra.BigOperators.Intervals |
| note | Mathlib does not contain the analogy between the geometric product and the arithmetic sum stated in terms of means. | The arithmetic-sum identity used here (sum equals count times average of endpoints) is captured in Mathlib via `Finset.sum_range_id` and related arithmetic-sum lemmas, but the explicit analogy with the geometric product is not stated. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
addedGeneral form a·r^nc0d1431f8e1a
addedExponential vs linear growthb049e23afdc8