`BookProof.ChapterPinDoubleCover.LamZ_spec_C` : ∀ S ∈ Omega, ∀ μ : Fin 4, mgamma μ * (Int.castRingHom ℂ).mapMatrix S = (Int.castRingHom ℂ).mapMatrix S * (∑ ν : Fin 4, (LamZ S) μ ν

Initializing...

`BookProof.ChapterPinDoubleCover.LamZ_spec_C` : ∀ S ∈ Omega, ∀ μ : Fin 4, mgamma μ * (Int.castRingHom ℂ).mapMatrix S = (Int.castRingHom ℂ).mapMatrix S * (∑ ν : Fin 4, (LamZ S) μ ν · Prove2Me