`BookProof.DirectSumEsa.subtype_comp_dsOpD` (A : ∀ i, D i →ₗ[ℂ] D i) : (dsCore D).subtype.comp (dsOpD A) = dsOp (fun i => (D i).subtype.comp (A i))

Initializing...

`BookProof.DirectSumEsa.subtype_comp_dsOpD` (A : ∀ i, D i →ₗ[ℂ] D i) : (dsCore D).subtype.comp (dsOpD A) = dsOp (fun i => (D i).subtype.comp (A i)) · Prove2Me