`BookProof.MixedLinearEsa.opL2_add` (A B : 𝓢(V, ℂ) →L[ℂ] 𝓢(V, ℂ)) : opL2 (A + B) = opL2 A + opL2 B

Initializing...

`BookProof.MixedLinearEsa.opL2_add` (A B : 𝓢(V, ℂ) →L[ℂ] 𝓢(V, ℂ)) : opL2 (A + B) = opL2 A + opL2 B · Prove2Me