`BookProof.NavierStokesGaugeY.genY_ccr_y` (j k : Fin 3) (p : NSAlg) : genY j (X (NSVar.y k) * p) - X (NSVar.y k) * genY j p = if j = k then p else 0

Initializing...

`BookProof.NavierStokesGaugeY.genY_ccr_y` (j k : Fin 3) (p : NSAlg) : genY j (X (NSVar.y k) * p) - X (NSVar.y k) * genY j p = if j = k then p else 0 · Prove2Me