Revision #2259 → #2909 · back to history
modifiedConjugation is an involutionb77546f80947
| Field | From #2259 | To #2909 |
|---|
| note | Verified: `Complex.conj_conj` (alias of `starRingEnd_self_apply`) gives `conj (conj x) = x`. | Verified: `Complex.conj_conj` is an alias of `starRingEnd_self_apply` giving `conj (conj x) = x`. |
addedNorm-squared (z · conj z)262cc018a327
addedUnit circle (unit complex numbers)df321f0e15f1
modifiedn-th roots of a complex numberac9b82a0765c
| Field | From #2259 | To #2909 |
|---|
| note | Verified: `Polynomial.nthRoots` (general definition) exists, but no single lemma enumerating the n distinct nth roots of an arbitrary complex number in polar form. | Verified: `Polynomial.nthRoots` exists generally, but no single lemma enumerates the n distinct nth roots of an arbitrary complex number in polar form. |
modifiedPolynomial ring R[X]3c99b7eeb3c7
| Field | From #2259 | To #2909 |
|---|
| note | Verified: `Polynomial R` is the standard polynomial-ring type over a semiring R. | Verified: `Polynomial R` is the standard polynomial-ring structure over a semiring R. |
addedAnalytic continuationcdae80536987
modifiedCauchy–Riemann characterization44e1f1a056c4
| Field | From #2259 | To #2909 |
|---|
| note | Verified via semantic search: this lemma states complex-differentiability ↔ real-differentiability + the Cauchy–Riemann identity `D f (i) = i · D f (1)`. | Verified: this lemma states complex-differentiability ↔ real-differentiability + the Cauchy–Riemann identity `D f (i) = i · D f (1)`. |
modifiedUnitary matrix9ff1316cc46f
| Field | From #2259 | To #2909 |
|---|
| note | Verified: `Matrix.unitaryGroup n α` (lowercase u) is the group of unitary matrices; cited `Matrix.UnitaryGroup` is only a namespace. | Verified: `Matrix.unitaryGroup n α` is the group of unitary matrices. |
addedFourier transform90fcb7b9995d