Prove2Me

BookProof.SpinStatistics.fermi_CAR_cross'

Proved
BookProof.SpinStatistics.fermi_CAR_cross_prime

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

BookProof.SpinStatistics.fermi_CAR_cross'

Preamble
-- Generated from ChapterSpinStatistics.lean — theorem BookProof.SpinStatistics.fermi_CAR_cross'
import Mathlib
import Definitions.Def_ChapterSpinStatistics
open BookProof.SpinStatistics



open Matrix
Formal statement
theorem BookProof.SpinStatistics.fermi_CAR_cross_prime : fermiAnnih2 * fermiCreate1 + fermiCreate1 * fermiAnnih2 = 0 := by sorry

View graph