therefore
Sign up
Open navigation
All proofs
Project-declaredLean 4.32.0 · mathlib@81a5d257c8e4

Self Adjoint ext

PauliMatrix.selfAdjoint_ext

physicsquantum field theoryrelativityself adjoint

Plain-language statement

Two 2×2 self-adjoint matrices are equal if the real traces of each matrix multiplied by each of the Pauli-matrices are equal.

Exact Lean statement

lemma selfAdjoint_ext {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}
    (h0 : ((Matrix.trace (σ0 * A.1))).re = ((Matrix.trace (σ0 * B.1))).re)
    (h1 : ((Matrix.trace (σ1 * A.1))).re = ((Matrix.trace (σ1 * B.1))).re)
    (h2 : ((Matrix.trace (σ2 * A.1))).re = ((Matrix.trace (σ2 * B.1))).re)
    (h3 : ((Matrix.trace (σ3 * A.1))).re = ((Matrix.trace (σ3 * B.1))).re) :
    A = B

Formal artifact

Lean source

Canonical source
Full Lean sourceLean 4
lemma selfAdjoint_ext {A B : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)}    (h0 : ((Matrix.trace (σ0 * A.1))).re = ((Matrix.trace (σ0 * B.1))).re)    (h1 : ((Matrix.trace (σ1 * A.1))).re = ((Matrix.trace (σ1 * B.1))).re)    (h2 : ((Matrix.trace (σ2 * A.1))).re = ((Matrix.trace (σ2 * B.1))).re)    (h3 : ((Matrix.trace (σ3 * A.1))).re = ((Matrix.trace (σ3 * B.1))).re) :    A = B := by  have h0' := congrArg ofRealHom h0  have h1' := congrArg ofRealHom h1  have h2' := congrArg ofRealHom h2  have h3' := congrArg ofRealHom h3  rw [ofRealHom_eq_coe, ofRealHom_eq_coe] at h0' h1' h2' h3'  rw [trace_pauliMatrix_mul_selfAdjoint_re _ A,    trace_pauliMatrix_mul_selfAdjoint_re _ B] at h0' h1' h2' h3'  exact selfAdjoint_ext_complex h0' h1' h2' h3'
Project
Physlib
License
Apache-2.0
Commit
dd43e9e65791
Source
Physlib/Relativity/PauliMatrices/SelfAdjoint.lean:63-76

Reuse this declaration

Bring the exact result into your workflow

The import identifies the source module. Your project still needs the pinned package dependency shown on this page.

What this badge means

This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.

Continue in this project

Related declarations

Project-declaredLean 4.32.0

Adiabatic relation log

adiabatic_relation_log

Plain-language statement

Adiabatic relation in logarithmic form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then c * log (Ua/Ub) + log (Va/Vb) = 0.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Adiabatic relation Ua Ub Va Vb

adiabatic_relation_UaUbVaVb

Plain-language statement

Adiabatic relation in product form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then (Ua/Ub)^c * (Va/Vb) = 1.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record