Revision #1326 → #2146 · back to history
modifiedPrincipal valueadb5c23aa7c3
| Field | From #1326 | To #2146 |
|---|
| note | Mathlib's arcsin/arccos/arctan are defined on their principal branches (e.g. range_arctan = Ioo (-(π/2)) (π/2)) but 'principal value' as a general concept is not separately introduced. | Mathlib's arcsin/arccos/arctan are defined on their principal branches (e.g. Real.arcsin_mem_Icc) but 'principal value' as a general concept is not separately introduced. |
modifiedCosine equation solution without plus-or-minus8a864fa186db
| Field | From #1326 | To #2146 |
|---|
| anchors | [{"section":"Solutions to elementary trigonometric equations","snippet":"With the help of integer parity"},{"type":"math_alttext","value":"{\\displaystyle \\operatorname {Parity} (h)={\\begin{cases}0&{\\text{if }}h{\\text{ is even }}\\\\1&{\\text{if }}h{\\text{ is odd }}\\\\\\end{cases}}}"}] | — |
modifiedPlus-or-minus symbol clarificationc8282cd996f6
| Field | From #1326 | To #2146 |
|---|
| anchors | [{"section":"Detailed example and explanation of the \"plus or minus\" symbol ±","snippet":"whose meaning is now clarified"},{"type":"math_alttext","value":"{\\displaystyle \\,\\theta =\\pm \\arccos x+2\\pi k\\,\\quad {\\text{ for some }}k\\in \\mathbb {Z} }"}] | — |
modifiedEqual trigonometric values relation4c2e4ec0d1ed
| Field | From #1326 | To #2146 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic | Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex |
| note | Some sin_eq_sin_iff style lemmas exist for periodic identification, but the full table of equality conditions is not assembled. | Real.sin_eq_sin_iff (in the Complex module) gives the periodic identification, but the full table of equality conditions across all six functions is not assembled. |
modifiedArctangent addition formula2f3d39e23b05
| Field | From #1326 | To #2146 |
|---|
| note | Real.arctan_add with the x*y<1 hypothesis, plus arctan_add_eq_add_pi/sub_pi for the other cases. | Real.arctan_add with the x*y<1 hypothesis, plus arctan_add_eq_add_pi for the other cases. |
modifiedGregory's series for arctangent7fa84c7e12b1
| Field | From #1326 | To #2146 |
|---|
| anchors | [{"section":"Infinite series","snippet":"The Taylor series for arctangent is also known as the arctangent series or Gregory's series"},{"type":"math_alttext","value":"{\\displaystyle {\\begin{aligned}\\arcsin(z)&=z+\\left({\\frac {1}{2}}\\right){\\frac {z^{3}}{3}}+\\left({\\frac {1\\cdot 3}{2\\cdot 4}}\\right){\\frac {z^{5}}{5}}+\\left({\\frac {1\\cdot 3\\cdot 5}{2\\cdot 4\\cdot 6}}\\right){\\frac {z^{7}}{7}}+\\cdots \\\\[5pt]&=\\sum _{n=0}^{\\infty }{\\frac {(2n-1)!!}{(2n)!!}}{\\frac {z^{2n+1}}{2n+1}}\\\\[5pt]&=\\sum _{n=0}^{\\infty }{\\frac {(2n)!}{(2^{n}n!)^{2}}}{\\frac {z^{2n+1}}{2n+1}}\\,;\\qquad |z|\\leq 1\\end{aligned}}}"},{"type":"math_alttext","value":"{\\displaystyle \\arctan(z)=z-{\\frac {z^{3}}{3}}+{\\frac {z^{5}}{5}}-{\\frac {z^{7}}{7}}+\\cdots =\\sum _{n=0}^{\\infty }{\\frac {(-1)^{n}z^{2n+1}}{2n+1}}\\,;\\qquad |z|\\leq 1\\qquad z\\neq i,-i}"}] | — |
addedTrigonometric functions are not one-to-one14188dee2d80
addedatan2 as principal argument of complex number5597a6bcb1e6