`BookProof.SmCar.car_annih_creat_of_ne` {i j : Fin n} (hij : i ≠ j) : annih i ∘ₗ creat j + creat j ∘ₗ annih i = 0

Initializing...

`BookProof.SmCar.car_annih_creat_of_ne` {i j : Fin n} (hij : i ≠ j) : annih i ∘ₗ creat j + creat j ∘ₗ annih i = 0 · Prove2Me