`BookProof.LorentzGroup.delta_card_four` : ({1, eta, -eta, -1} : Finset (Matrix (Fin 4) (Fin 4) ℝ)).card = 4

Initializing...

`BookProof.LorentzGroup.delta_card_four` : ({1, eta, -eta, -1} : Finset (Matrix (Fin 4) (Fin 4) ℝ)).card = 4 · Prove2Me