Revision #1863 → #3356 · back to history
modifiedSquare root of 2342cf00fd3dc
| Field | From #1863 | To #3356 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Pow.NNReal | Mathlib.Analysis.Real.Sqrt |
| note | Mathlib has `Real.sqrt 2` with `Real.sq_sqrt`/`Real.sqrt_sq` characterizing it as the unique nonnegative real squaring to 2. | `Real.sqrt` is defined in `Mathlib.Analysis.Real.Sqrt`; `Real.sq_sqrt`/`Real.sqrt_sq` characterize `Real.sqrt 2` as the unique nonnegative real squaring to 2. |
addedContinued fraction of √2 is periodic63518524532d
addedGaussian integral3dc990262ab3
addedComplex roots of unity34679855e207
modifiedDefinition of e2395ee3fffee
| Field | From #1863 | To #3356 |
|---|
| mathlib.module | Mathlib.Data.Complex.Exponential | Mathlib.Analysis.Complex.Exponential |
| note | Euler's number is `Real.exp 1`; the limit definition `(1+1/n)^n → e` is the special case of `tendsto_one_add_div_pow_exp` at `t = 1`. | Euler's number is `Real.exp 1`; the limit definition `(1+1/n)^n → e` is the `t = 1` special case of `Real.tendsto_one_add_div_pow_exp`. |
modifiede and the exponential function2bf3f1c75a54
| Field | From #1863 | To #3356 |
|---|
| mathlib.module | Mathlib.Data.Complex.Exponential | Mathlib.Analysis.Complex.Exponential |
addedFibonacci sequence0d8ad0188774
addedRiemann zeta function32a3d15880b8
addedDirichlet beta function4fe52df7b306
modified0.999... equals 13e690162cd91
| Field | From #1863 | To #3356 |
|---|
| note | `ofDigits_const_last_eq_one` proves the base-b identity `0.(b-1)(b-1)… = 1`, which specializes at `b = 10` to `0.999… = 1`. | `Real.ofDigits_const_last_eq_one` states `ofDigits (fun _ ↦ Fin.last b) = 1`, explicitly documented as a generalization of the identity `0.(9) = 1`. |
| provenance | ai | ai-moderated |