Revision #2541 → #3589 · back to history
modifiedComplex conjugate root theoreme52025aef33b
| Field | From #2541 | To #3589 |
|---|
| note | `RCLike.aeval_conj` gives `aeval (conj z) p = conj (aeval z p)` for `p : ℝ[X]`, immediately yielding the conjugate-root theorem (used as `simpa [dvd_iff_isRoot, aeval_conj]` in `Analysis/Complex/Polynomial/Basic.lean`). | `Polynomial.aeval_conj` gives `aeval (conj z) p = conj (aeval z p)` for `p : ℝ[X]`, immediately yielding the conjugate-root theorem (used as `simpa [dvd_iff_isRoot, aeval_conj]` in `Analysis/Complex/Polynomial/Basic.lean`). |
modifiedConjugation preserves modulus5b51a429960d
| Field | From #2541 | To #3589 |
|---|
| mathlib.module | Mathlib.Analysis.Complex.Basic | Mathlib.Analysis.Complex.Norm |
addedMultiplicative inverse via conjugate9b78c17aa3f5
modifiedConjugation commutes with exp, log, integer powers923344b73011
| Field | From #2541 | To #3589 |
|---|
| mathlib.module | Mathlib.Data.Complex.Exponential | Mathlib.Analysis.Complex.Exponential |
| note | `Complex.exp_conj` (used in `JacobiTheta`) and `Complex.log_conj` (in `Analysis/SpecialFunctions/Complex/Log.lean:123`, with side hypothesis `x.arg ≠ π`) give the exp/log cases; integer-power compatibility follows from `map_pow`/`map_zpow` on the ring homomorphism `starRingEnd ℂ`. | `Complex.exp_conj` and `Complex.log_conj` (in `Analysis/SpecialFunctions/Complex/Log.lean`, with side hypothesis `x.arg ≠ π`) give the exp/log cases; integer-power compatibility follows from `map_pow`/`map_zpow` on the ring homomorphism `starRingEnd ℂ`. |
modifiedReal polynomial roots in conjugate pairsc81429d097f2
| Field | From #2541 | To #3589 |
|---|
| note | `RCLike.aeval_conj` is the workhorse and is invoked (via `simpa [dvd_iff_isRoot, aeval_conj]`) in `Analysis/Complex/Polynomial/Basic.lean:180` precisely to derive that non-real roots come in conjugate pairs. | `Polynomial.aeval_conj` is the workhorse and is invoked (via `simpa [dvd_iff_isRoot, aeval_conj]`) in `Analysis/Complex/Polynomial/Basic.lean:180` precisely to derive that non-real roots come in conjugate pairs. |
modifiedElement-wise conjugation on matricesb49662995c3b
| Field | From #2541 | To #3589 |
|---|
| label | Conjugation on matrices | Element-wise conjugation on matrices |
| mathlib.decl | Matrix.conjTranspose | — |
| mathlib.match_kind | exact | — |
| mathlib.module | Mathlib.LinearAlgebra.Matrix.ConjTranspose | — |
| note | `Matrix.conjTranspose` (notation `ᴴ`) is defined and packaged as a star operation, additive equiv, linear map, and (in the square case) a `StarRingEquiv` to the opposite ring. | Element-wise conjugation of a complex matrix is written in Mathlib as `M.map (starRingEnd ℂ)` (or `M.map conj`) via `Matrix.map`; there is no dedicated `Matrix.conj` decl. Distinct from `Matrix.conjTranspose` (see the conjugate-transpose annotation). |
| provenance | ai | ai-moderated |
| status | formalized | partial |
addedConjugate transpose of a matrixdda3f26bdf51
addedAdjoint operator on Hilbert spaces30847b6f450f
added*-operation of a C*-algebraf966f89f9e36
modifiedQuaternion conjugation8a442b81f538
| Field | From #2541 | To #3589 |
|---|
| note | Quaternion conjugation is the `star` of `Quaternion.instStarRing` (line 605, `star_involutive x := by simp [Star.star]`), with companion lemmas `Quaternion.star_mul_self`, `self_mul_star`, etc. | Quaternion conjugation is the `star` of `Quaternion.instStarRing`, with companion lemmas `Quaternion.star_mul_self`, `self_mul_star`, etc. |
modifiedGeneralized conjugation is multiplicative with reversal1465bc628c46
| Field | From #2541 | To #3589 |
|---|
| note | `StarMul.star_mul : ∀ r s, star (r * s) = star s * star r` (line 123) is exactly the antimultiplicative-with-reversal property satisfied by complex, matrix, quaternion star operations. | `StarMul.star_mul : ∀ r s, star (r * s) = star s * star r` is exactly the antimultiplicative-with-reversal property satisfied by complex, matrix, quaternion star operations. |
modifiedComplex conjugation / real structure on a vector spaceb5669639ff4d
| Field | From #2541 | To #3589 |
|---|
| mathlib.module | Mathlib.Algebra.Star.Module | Mathlib.Algebra.Star.Basic |