`BookProof.DirectSumEsa.dsOpD_isSymmetricDom` (A : ∀ i, D i →ₗ[ℂ] D i) (hsym : ∀ i, IsSymmetricDom (A i)) : IsSymmetricDom (dsOpD A)

Initializing...

`BookProof.DirectSumEsa.dsOpD_isSymmetricDom` (A : ∀ i, D i →ₗ[ℂ] D i) (hsym : ∀ i, IsSymmetricDom (A i)) : IsSymmetricDom (dsOpD A) · Prove2Me