Revision #3629 → #4184 · back to history
modifiedTrigonometric functions (Surya Siddhanta)33be860c2c46
| Field | From #3629 | To #4184 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | Mathlib.Analysis.Complex.Trigonometric |
modifiedDefinition of sine (Aryabhata)34f29d0d2b73
| Field | From #3629 | To #4184 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | Mathlib.Analysis.Complex.Trigonometric |
modifiedSum of cubes formula (Aryabhata)d808aeee66c8
| Field | From #3629 | To #4184 |
|---|
| mathlib.decl | — | sum_range_pow |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.NumberTheory.Bernoulli |
| note | No closed-form lemma for ∑i³ exists in Mathlib (only the linear Gauss sum Finset.sum_range_id). | Mathlib has Faulhaber's formula sum_range_pow via Bernoulli numbers, which specializes to the sum-of-cubes closed form (n(n+1)/2)² but the concrete cube case is not a separately stated lemma. |
| provenance | ai | ai-moderated |
| status | not_formalized | partial |
modifiedSine-cosine relations (Varahamihira)655cd3521603
| Field | From #3629 | To #4184 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | Mathlib.Analysis.Complex.Trigonometric |
modifiedArithmetic rules for zero and negatives (Brahmagupta)e23a01d7a73a
| Field | From #3629 | To #4184 |
|---|
| mathlib.decl | mul_zero | MulZeroClass.mul_zero |
| mathlib.module | Mathlib.Algebra.GroupWithZero.Basic | Mathlib.Algebra.GroupWithZero.Defs |
| note | These are basic ring/field lemmas in Mathlib (mul_zero, add_zero, neg_neg, neg_mul, etc.). | These are basic ring/field lemmas in Mathlib (MulZeroClass.mul_zero, add_zero, neg_neg, neg_mul, etc.). |
addedFibonacci numbers (Pingala)bfb09135c3ae
addedSquare root of two is irrational444c5f1120af
addedHeron's formula (generalization)14708a4c4afb