`BookProof.NsBrstDerivativeGauge.nsDerivBrstCharge2_apply_tmul` (p : NSAlg) (w : nsGhostSpace) : nsDerivBrstCharge2 (p ⊗ₜ[ℂ] w) = ∑ j : Fin 3, genY2 j p ⊗ₜ[ℂ] nsGhostCre j w

Initializing...

`BookProof.NsBrstDerivativeGauge.nsDerivBrstCharge2_apply_tmul` (p : NSAlg) (w : nsGhostSpace) : nsDerivBrstCharge2 (p ⊗ₜ[ℂ] w) = ∑ j : Fin 3, genY2 j p ⊗ₜ[ℂ] nsGhostCre j w · Prove2Me