WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Imaginary unit

Revision #1312 → #2728 · back to history

modifiedImaginary unitd3719bd4fd8a
FieldFrom #1312To #2728
mathlib.decl—Complex.I
mathlib.match_kind—exact
mathlib.module—Mathlib.Data.Complex.Basic
note—Complex.I is the definition of the imaginary unit as a solution of x² = -1.
status—formalized
modifiedImaginary number835f2837c342
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—There is no dedicated `ImaginaryNumber` predicate or subset in Mathlib; imaginary numbers are represented pointwise as `x * I` with `x : ℝ`.
status—not_formalized
modifiedComplex numbers143d1d67093e
FieldFrom #1312To #2728
mathlib.decl—Complex
mathlib.match_kind—exact
mathlib.module—Mathlib.Data.Complex.Basic
note—The `Complex` structure defines the complex numbers as pairs of reals with the usual field operations.
status—formalized
modifiedTwo complex square roots of −1a2e2b19ba45f
FieldFrom #1312To #2728
mathlib.decl—Complex.I_sq
mathlib.match_kind—special_case
mathlib.module—Mathlib.Data.Complex.Basic
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.
status—partial
modifiedSquare roots of nonzero complex numbers229aa290e356
FieldFrom #1312To #2728
mathlib.decl—Complex.sqrt
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.RCLike.Sqrt
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.
status—partial
modifiedDefining property of i84a4b0f6df1c
FieldFrom #1312To #2728
mathlib.decl—Complex.I_sq
mathlib.match_kind—exact
mathlib.module—Mathlib.Data.Complex.Basic
note—`Complex.I_sq` states `I ^ 2 = -1`.
status—formalized
modifiedi and −i are square roots of −175eb3e887675
FieldFrom #1312To #2728
mathlib.decl—Complex.I_sq
mathlib.match_kind—special_case
mathlib.module—Mathlib.Data.Complex.Basic
note—`Complex.I_sq` gives `I^2 = -1`; the analogous `(-I)^2 = -1` is a trivial corollary but not separately named.
status—partial
modifiedPowers of i cycle931757066099
FieldFrom #1312To #2728
mathlib.decl—Complex.I_sq
mathlib.match_kind—special_case
mathlib.module—Mathlib.Data.Complex.Basic
note—Ingredients `Complex.I_sq` and `Complex.I_mul_I` are available, but no lemma packages the length-4 cycle of `I^n` explicitly.
status—partial
modifiedRectangular and polar form of ib762e7e2d416
FieldFrom #1312To #2728
mathlib.decl—Complex.I_re
mathlib.match_kind—exact
mathlib.module—Mathlib.Data.Complex.Basic
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`.
status—formalized
modifiedTwo distinct solutions of x²=−19ee0c363e4c5
FieldFrom #1312To #2728
mathlib.decl—Complex.I_sq
mathlib.match_kind—special_case
mathlib.module—Mathlib.Data.Complex.Basic
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.
status—partial
modifiedTwo automorphisms fixing the realsca2d767ef12f
FieldFrom #1312To #2728
mathlib.decl—Complex.uniformContinuous_ringHom_eq_id_or_conj
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.Instances.Complex
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.
status—partial
modifiedMatrix representation of complex numbersc1b62ecbf0a8
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No general `Complex → Matrix` ring embedding with the described defining relations is packaged in Mathlib.
status—not_formalized
modifiedIdentity matrix representation12bd506581e2
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The canonical `[[0,-1],[1,0]]` representation of `I` is not defined as a Mathlib construction.
status—not_formalized
modifiedGeneral trace-zero determinant-one J4ac9e047b9cc
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The 2×2 Cayley-Hamilton corollary that trace 0, det 1 forces `J^2 = -I` is not packaged as a named lemma.
status—not_formalized
modifiedPolynomial ring over reals62224856ea7e
FieldFrom #1312To #2728
mathlib.decl—Polynomial
mathlib.match_kind—generalization
mathlib.module—Mathlib.Algebra.Polynomial.Basic
note—`Polynomial ℝ` is a special case of the general `Polynomial R` construction.
status—formalized
modifiedQuotient ring isomorphic to complex numbers958426258e46
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No explicit `ℝ[X]/(X²+1) ≃ ℂ` isomorphism is packaged in Mathlib (searches for `AdjoinRoot`/`Polynomial.quotient` mapping to `Complex` returned no matches).
status—not_formalized
modifiedComplex plane37a97f5d3625
FieldFrom #1312To #2728
mathlib.decl—Complex.equivRealProd
mathlib.match_kind—exact
mathlib.module—Mathlib.Data.Complex.Basic
note—`Complex.equivRealProd` is the identification of `ℂ` with `ℝ × ℝ` underlying the complex plane.
status—formalized
modifiedMultiplication as rotation546a5bf61b91
FieldFrom #1312To #2728
mathlib.decl—Complex.rotation
mathlib.match_kind—exact
mathlib.module—Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
note—`Complex.rotation` identifies multiplication by `exp(θ·I)` with the oriented rotation by θ.
status—formalized
modifiedSimilarity transformations as complex-linear9e556b25c9ce
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No packaged identification of planar similarities with complex-affine maps `z ↦ az+b` was found.
status—not_formalized
modifiedSquares of vectors and bivectors27d7200a890e
FieldFrom #1312To #2728
mathlib.decl—CliffordAlgebra.ι_sq_scalar
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.CliffordAlgebra.Basic
note—General clifford algebra provides `ι(v)^2 = Q(v)`; the specific 'positive for vectors, negative for bivectors' packaging is not named.
status—partial
modifiedUnit bivector as imaginary unitf69128acb259
FieldFrom #1312To #2728
mathlib.decl—CliffordAlgebraComplex.ofComplex
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
note—`CliffordAlgebraComplex.equiv` realizes `ℂ` as the Clifford algebra of the negative-definite one-dim real form, sending `I` to the unit bivector.
status—formalized
modifiedBivector algebra isomorphic to complex1657d1b8cad2
FieldFrom #1312To #2728
mathlib.decl—CliffordAlgebraComplex.equiv
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
note—`CliffordAlgebraComplex.equiv` gives the ℝ-algebra equivalence between this Clifford algebra and `ℂ`.
status—formalized
modifiedHigher-dimensional unit bivectorc21eef96d23a
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma about unit bivectors of arbitrary planar orientation squaring to -1 in higher-dim Clifford algebras is packaged.
status—not_formalized
modifiedRadical rules valid only for positive reals23b6e9099ade
FieldFrom #1312To #2728
mathlib.decl—Real.sqrt_mul
mathlib.match_kind—special_case
mathlib.module—Mathlib.Analysis.SpecialFunctions.Pow.NNReal
note—`Real.sqrt_mul` gives the multiplicativity of `√` under a nonnegativity hypothesis; the failure/caveat statement itself isn't packaged.
status—partial
modifiedImaginary integer50179ec013cf
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No dedicated `ImaginaryInt` definition exists; such numbers appear only as terms `n * I`.
status—not_formalized
modifiedImaginary unit generates infinite cyclic groupea5d32b5c819
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma states that the additive subgroup `ℤ · I ≤ ℂ` is an infinite cyclic group generated by `I`.
status—not_formalized
modifiedImaginary axise9a5c5448380
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The imaginary axis is not defined as a Mathlib object; only its element-wise predicate `re = 0` is available.
status—not_formalized
modifiedGaussian integers75b925dad490
FieldFrom #1312To #2728
mathlib.decl—GaussianInt
mathlib.match_kind—exact
mathlib.module—Mathlib.NumberTheory.Zsqrtd.GaussianInt
note—`GaussianInt` is defined as `Zsqrtd (-1)`, i.e., `ℤ[i]`.
status—formalized
modifiedClosure of Gaussian integers698ce4b48298
FieldFrom #1312To #2728
mathlib.decl—GaussianInt.instCommRing
mathlib.match_kind—exact
mathlib.module—Mathlib.NumberTheory.Zsqrtd.GaussianInt
note—The `CommRing` instance on `GaussianInt` encodes closure under sum, difference, and product.
status—formalized
modifiedMultiplication by i as quarter turnb490aa9a7206
FieldFrom #1312To #2728
mathlib.decl—Complex.rotation
mathlib.match_kind—special_case
mathlib.module—Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
note—The generic `Complex.rotation` covers multiplication by `exp(iθ)` as an oriented rotation; the specific θ = π/2 quarter-turn instance is not named.
status—partial
modifiedi generates cyclic group of order 4509d541b859d
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `orderOf Complex.I = 4` lemma or explicit `⟨I⟩` cyclic-subgroup statement is packaged.
status—not_formalized
modifiedEuler's formula special casef2aa32b8a24e
FieldFrom #1312To #2728
mathlib.decl—Complex.exp_mul_I
mathlib.match_kind—generalization
mathlib.module—Mathlib.Analysis.Complex.Trigonometric
note—`Complex.exp_mul_I` gives `exp(x·I) = cos x + sin x · I`, which specializes to `I^n = exp(n·π/2·I)`.
status—formalized
modifiedTwo square roots of i53fe2e742c6e
FieldFrom #1312To #2728
mathlib.decl—Complex.sqrt_I
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.RCLike.Sqrt
note—`Complex.sqrt_I : sqrt I = √2⁻¹ * (1 + I)` gives one root explicitly; the additive-inverse root follows from `sqrt` conventions.
status—formalized
addedCube roots of id79809f20f88
modifiedn-th roots of ie7ba0a46dde4
FieldFrom #1312To #2728
mathlib.decl—Complex.isPrimitiveRoot_exp
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.RootsOfUnity.Complex
note—General roots-of-unity theory is available, but no lemma enumerates the `n`-th roots of `I` specifically.
status—partial
modifiedRoots as regular polygon vertices7603670133d7
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma stating that `n`-th roots of `I` form a regular polygon on the unit circle.
status—not_formalized
modifiedComplex exponential periodicity95e7ea846474
FieldFrom #1312To #2728
mathlib.decl—Complex.exp_periodic
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
note—`Complex.exp_periodic : Function.Periodic exp (2 * π * I)`.
status—formalized
addedExponential decomposes into cosh and sinh0a7df66d9858
modifiedEuler's formulabfef19f4d008
FieldFrom #1312To #2728
mathlib.decl—Complex.exp_mul_I
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Complex.Trigonometric
note—`Complex.exp_mul_I : exp (x * I) = cos x + sin x * I` is Euler's formula.
status—formalized
modifiedi^i is real13a2e732f0e0
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No lemma computes `I ^ I = exp(-π/2)` (or its multi-valued form) in Mathlib.
status—not_formalized
modifiedPartial fraction for coth767b9c2d2100
FieldFrom #1312To #2728
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Mittag-Leffler partial-fraction expansion of `coth` (or `π cot πz`) is not packaged in Mathlib.
status—not_formalized
modifiedComplex logarithm is multi-valued8ef2c8afb22a
FieldFrom #1312To #2728
mathlib.decl—Complex.log
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.SpecialFunctions.Complex.Log
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.
status—partial
modifiedFactorial of i via gamma functionfe8e7f892a4d
FieldFrom #1312To #2728
mathlib.decl—Complex.Gamma
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.SpecialFunctions.Gamma.Basic
note—`Complex.Gamma` is available, so `Gamma (1 + I)` is a well-formed term, but the specific value/expression for `i!` is not stated.
status—partial