Revision #3058 → #4352 · back to history
modifiedImaginary unitd3719bd4fd8a
| Field | From #3058 | To #4352 |
|---|
| note | Complex.I is the definition of the imaginary unit as a solution of x² = -1. | `Complex.I` is the imaginary unit, defined so that `I^2 = -1` (verified). |
modifiedImaginary number835f2837c342
| Field | From #3058 | To #4352 |
|---|
| note | There is no dedicated `ImaginaryNumber` predicate or subset in Mathlib; imaginary numbers are represented pointwise as `x * I` with `x : ℝ`. | No dedicated predicate/subset for imaginary numbers in Mathlib; they appear as terms `x * I` for real `x`. |
modifiedComplex numbers143d1d67093e
| Field | From #3058 | To #4352 |
|---|
| note | The `Complex` structure defines the complex numbers as pairs of reals with the usual field operations. | `Complex` is Mathlib's complex number structure (verified). |
modifiedTwo complex square roots of −1a2e2b19ba45f
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.I_sq : I^2 = -1` (and by negation `(-I)^2 = -1`) shows both roots, but no packaged 'exactly two roots' statement targets `-1` specifically. | `Complex.I_sq` gives one root; no 'exactly two square roots of -1' lemma is packaged. |
modifiedSquare roots of nonzero complex numbers229aa290e356
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.sqrt` gives one root and (with negation) the other; algebraic closure via `Complex.exists_root` covers existence, but the two-distinct-roots-for-nonzero packaging is not a stand-alone lemma. | `Complex.sqrt` plus `Complex.exists_root` give the ingredients but the exact 'two distinct square roots for nonzero `z`' lemma is not packaged. |
modifiedDefining property of i84a4b0f6df1c
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.I_sq` states `I ^ 2 = -1`. | `Complex.I_sq : I ^ 2 = -1` (verified). |
modifiedi and −i are square roots of −175eb3e887675
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.I_sq` gives `I^2 = -1`; the analogous `(-I)^2 = -1` is a trivial corollary but not separately named. | `Complex.I_sq` covers `I^2 = -1`; `(-I)^2 = -1` is a trivial corollary but not separately named. |
modifiedPowers of i cycle931757066099
| Field | From #3058 | To #4352 |
|---|
| note | Ingredients `Complex.I_sq` and `Complex.I_mul_I` are available, but no lemma packages the length-4 cycle of `I^n` explicitly. | `Complex.I_sq` and `Complex.I_mul_I` are available but no length-4 cycle lemma for `I^n` is packaged. |
modifiedRectangular and polar form of ib762e7e2d416
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.I_re = 0`, `Complex.I_im = 1`, `Complex.norm_I = 1`, and `Complex.arg_I = π/2` give both rectangular and polar coordinates of `I`. | `Complex.I_re = 0`, `Complex.I_im = 1`, `Complex.norm_I = 1`, `Complex.arg_I = π/2` give rectangular and polar coordinates. |
modifiedTwo distinct solutions of x²=−19ee0c363e4c5
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.I_sq` and `Complex.I_ne_zero` show both `I` and `-I` are distinct roots, but no combined 'exactly two solutions of x^2=-1' lemma exists. | `Complex.I_sq` and `Complex.I_ne_zero` give the ingredients; no combined 'exactly two solutions of x²=-1' lemma. |
modifiedTwo automorphisms fixing the realsca2d767ef12f
| Field | From #3058 | To #4352 |
|---|
| note | This shows any uniformly continuous ring hom on a subfield extends to the identity or conjugation; the pure algebraic 'exactly two ℝ-fixing automorphisms' statement is not separately packaged. | This lemma handles any uniformly continuous ring hom; the pure algebraic 'exactly two ℝ-fixing automorphisms' statement is not separately packaged. |
modifiedMatrix representation of complex numbersc1b62ecbf0a8
| Field | From #3058 | To #4352 |
|---|
| note | No general `Complex → Matrix` ring embedding with the described defining relations is packaged in Mathlib. | No general `Complex → Matrix` ring embedding with the stated defining relations is packaged. |
modifiedIdentity matrix representation12bd506581e2
| Field | From #3058 | To #4352 |
|---|
| note | The canonical `[[0,-1],[1,0]]` representation of `I` is not defined as a Mathlib construction. | The canonical `[[0,-1],[1,0]]` representation of `I` is not packaged as a Mathlib construction. |
modifiedGeneral trace-zero determinant-one J4ac9e047b9cc
| Field | From #3058 | To #4352 |
|---|
| note | The 2×2 Cayley-Hamilton corollary that trace 0, det 1 forces `J^2 = -I` is not packaged as a named lemma. | The 2×2 Cayley–Hamilton corollary that trace 0, det 1 forces `J^2 = -I` is not packaged as a named lemma. |
modifiedQuotient ring isomorphic to complex numbers958426258e46
| Field | From #3058 | To #4352 |
|---|
| note | No explicit `ℝ[X]/(X²+1) ≃ ℂ` isomorphism is packaged in Mathlib (searches for `AdjoinRoot`/`Polynomial.quotient` mapping to `Complex` returned no matches). | No explicit `ℝ[X]/(X²+1) ≃ ℂ` isomorphism found in Mathlib. |
modifiedComplex plane37a97f5d3625
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.equivRealProd` is the identification of `ℂ` with `ℝ × ℝ` underlying the complex plane. | `Complex.equivRealProd` identifies `ℂ` with `ℝ × ℝ`, the complex-plane coordinate map. |
addedAddition as translation in the planeb22bde3a2db3
modifiedMultiplication as rotation546a5bf61b91
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.rotation` identifies multiplication by `exp(θ·I)` with the oriented rotation by θ. | `Complex.rotation` identifies multiplication by `exp(θ·I)` with the oriented plane rotation by `θ`. |
modifiedSimilarity transformations as complex-linear9e556b25c9ce
| Field | From #3058 | To #4352 |
|---|
| note | No packaged identification of planar similarities with complex-affine maps `z ↦ az+b` was found. | No identification of planar similarities with complex-affine maps `z ↦ az+b` found in Mathlib. |
modifiedSquares of vectors and bivectors27d7200a890e
| Field | From #3058 | To #4352 |
|---|
| note | General clifford algebra provides `ι(v)^2 = Q(v)`; the specific 'positive for vectors, negative for bivectors' packaging is not named. | `CliffordAlgebra.ι_sq_scalar` says `ι(v)^2 = Q(v)` for any quadratic form; the vector/bivector sign dichotomy is not separately named. |
modifiedUnit bivector as imaginary unitf69128acb259
| Field | From #3058 | To #4352 |
|---|
| note | `CliffordAlgebraComplex.equiv` realizes `ℂ` as the Clifford algebra of the negative-definite one-dim real form, sending `I` to the unit bivector. | `CliffordAlgebraComplex.ofComplex` sends `I` to the unit bivector `ι(1)` of the negative-definite 1-dim real Clifford algebra. |
modifiedBivector algebra isomorphic to complex1657d1b8cad2
| Field | From #3058 | To #4352 |
|---|
| note | `CliffordAlgebraComplex.equiv` gives the ℝ-algebra equivalence between this Clifford algebra and `ℂ`. | `CliffordAlgebraComplex.equiv` is the ℝ-algebra equivalence between this Clifford algebra and `ℂ`. |
modifiedHigher-dimensional unit bivectorc21eef96d23a
| Field | From #3058 | To #4352 |
|---|
| note | No lemma about unit bivectors of arbitrary planar orientation squaring to -1 in higher-dim Clifford algebras is packaged. | No lemma on arbitrary unit bivectors squaring to -1 in higher-dim Clifford algebras is packaged. |
modifiedRadical rules valid only for positive reals23b6e9099ade
| Field | From #3058 | To #4352 |
|---|
| mathlib.module | Mathlib.Analysis.SpecialFunctions.Pow.NNReal | Mathlib.Analysis.Real.Sqrt |
| note | `Real.sqrt_mul` gives the multiplicativity of `√` under a nonnegativity hypothesis; the failure/caveat statement itself isn't packaged. | `Real.sqrt_mul` gives multiplicativity of `√` under nonnegativity; the failure/caveat for complex arguments itself is not packaged. |
modifiedImaginary integer50179ec013cf
| Field | From #3058 | To #4352 |
|---|
| note | No dedicated `ImaginaryInt` definition exists; such numbers appear only as terms `n * I`. | No `ImaginaryInt` type/predicate; such numbers appear only as terms `n * I`. |
modifiedImaginary unit generates infinite cyclic groupea5d32b5c819
| Field | From #3058 | To #4352 |
|---|
| note | No lemma states that the additive subgroup `ℤ · I ≤ ℂ` is an infinite cyclic group generated by `I`. | No lemma stating that `ℤ · I ≤ ℂ` is an infinite cyclic subgroup generated by `I`. |
modifiedImaginary axise9a5c5448380
| Field | From #3058 | To #4352 |
|---|
| note | The imaginary axis is not defined as a Mathlib object; only its element-wise predicate `re = 0` is available. | The imaginary axis is not defined as a Mathlib object; only its elementwise predicate `re = 0` is available. |
modifiedGaussian integers75b925dad490
| Field | From #3058 | To #4352 |
|---|
| note | `GaussianInt` is defined as `Zsqrtd (-1)`, i.e., `ℤ[i]`. | `GaussianInt` is defined as `Zsqrtd (-1)`, i.e., `ℤ[i]` (verified). |
modifiedMultiplication by i as quarter turnb490aa9a7206
| Field | From #3058 | To #4352 |
|---|
| note | The generic `Complex.rotation` covers multiplication by `exp(iθ)` as an oriented rotation; the specific θ = π/2 quarter-turn instance is not named. | `Complex.rotation` covers all `exp(iθ)`-multiplications; the θ = π/2 'quarter-turn' instance is not separately named. |
modifiedi generates cyclic group of order 4509d541b859d
| Field | From #3058 | To #4352 |
|---|
| note | No `orderOf Complex.I = 4` lemma or explicit `⟨I⟩` cyclic-subgroup statement is packaged. | No `orderOf Complex.I = 4` or `⟨I⟩` cyclic-subgroup statement is packaged. |
modifiedEuler's formula special casef2aa32b8a24e
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.exp_mul_I` gives `exp(x·I) = cos x + sin x · I`, which specializes to `I^n = exp(n·π/2·I)`. | `Complex.exp_mul_I : exp (x * I) = cos x + sin x * I`, specializing at `x = n·π/2` to `I^n`. |
modifiedTwo square roots of i53fe2e742c6e
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.sqrt_I : sqrt I = √2⁻¹ * (1 + I)` gives one root explicitly; the additive-inverse root follows from `sqrt` conventions. | `Complex.sqrt_I` gives one root explicitly; the additive-inverse root follows from `sqrt` conventions. |
modifiedn-th roots of ie7ba0a46dde4
| Field | From #3058 | To #4352 |
|---|
| note | General roots-of-unity theory is available, but no lemma enumerates the `n`-th roots of `I` specifically. | General roots-of-unity theory is available; no enumeration of `n`-th roots of `I` specifically. |
modifiedComplex exponential periodicity95e7ea846474
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.exp_periodic : Function.Periodic exp (2 * π * I)`. | `Complex.exp_periodic : Function.Periodic exp (2 * π * I)` (verified). |
modifiedExponential decomposes into cosh and sinh0a7df66d9858
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.cosh_add_sinh : cosh x + sinh x = exp x` gives the even/odd decomposition. | `Complex.cosh_add_sinh : cosh x + sinh x = exp x` is the even/odd decomposition. |
modifiedi^i is real13a2e732f0e0
| Field | From #3058 | To #4352 |
|---|
| note | No lemma computes `I ^ I = exp(-π/2)` (or its multi-valued form) in Mathlib. | No lemma computes `I ^ I = exp(-π/2)` in Mathlib. |
modifiedPartial fraction for coth767b9c2d2100
| Field | From #3058 | To #4352 |
|---|
| note | The Mittag-Leffler partial-fraction expansion of `coth` (or `π cot πz`) is not packaged in Mathlib. | The Mittag-Leffler partial-fraction expansion of `coth` is not packaged in Mathlib. |
modifiedComplex logarithm is multi-valued8ef2c8afb22a
| Field | From #3058 | To #4352 |
|---|
| note | Mathlib's `Complex.log` is a specific principal branch; the multi-valuedness (as `log z + 2πik`) is implicit via `Complex.exp_periodic` but not packaged as such. | `Complex.log` is only the principal branch; multi-valuedness `log z + 2πik` is implicit via `Complex.exp_periodic` but not packaged as such. |
modifiedFactorial of i via gamma functionfe8e7f892a4d
| Field | From #3058 | To #4352 |
|---|
| note | `Complex.Gamma` is available, so `Gamma (1 + I)` is a well-formed term, but the specific value/expression for `i!` is not stated. | `Complex.Gamma` is defined so `Gamma (1 + I)` is a well-formed term, but the specific value/expression for `i!` is not stated. |