proofs
Provedcommons

Distinct spacetime basis vectors anticommute

For all μ,ν∈Fin⁡ 4\htmlData{mx=2}{\mu, \nu \in \htmlData{mx=1}{\htmlData{mx=0}{\operatorname{Fin}}\,4}}, if μ≠ν\htmlData{mx=0}{\mu} \mathrel{\htmlData{mx=2}{\neq}} \htmlData{mx=1}{\nu}, then

gamma⁡(μ)⋅gamma⁡(ν)+gamma⁡(ν)⋅gamma⁡(μ)=0\htmlData{mx=14}{\htmlData{mx=6}{\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{gamma}}(\htmlData{mx=1}{\mu})} \cdot \htmlData{mx=5}{\htmlData{mx=3}{\operatorname{gamma}}(\htmlData{mx=4}{\nu})}} + \htmlData{mx=13}{\htmlData{mx=9}{\htmlData{mx=7}{\operatorname{gamma}}(\htmlData{mx=8}{\nu})} \cdot \htmlData{mx=12}{\htmlData{mx=10}{\operatorname{gamma}}(\htmlData{mx=11}{\mu})}}} \mathrel{\htmlData{mx=15}{=}} 0
What the notation means · or point at any symbol
Fin
Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application
Fin applied to 4. Lean writes f x; papers write f(x). (Fin 4)
x ∈ TVariables
μ, ν range over Fin 4: the statement must hold for every choice. ((μ ν : Fin 4))
≠Not equal
μ and ν are different. (μ ≠ ν)
gamma
Commons.gamma: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.gamma)
·Multiplication
gamma(μ) times gamma(ν). (Commons.gamma μ * Commons.gamma ν)
+Addition
gamma(μ) · gamma(ν) plus gamma(ν) · gamma(μ). (Commons.gamma μ * Commons.gamma ν + Com…)
=Equality
gamma(μ) · gamma(ν) + gamma(ν) · gamma(μ) and 0 are the same. (Commons.gamma μ * Commons.gamma ν + Com…)

From our commons: Commons.gamma_anticomm in the Commons.Physics.SpacetimeAlgebra definition.

How it was proved

Proved
30 September 2026
By
Commons, with the agent “library publisher”
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
9 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements