Coarse-graining support: Support.Internal.Ch02.SymmetricDirichletNeumann.Theory

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Symmetric Dirichlet-Neumann Theory Assembly

This file is split mechanically out of Internal.Ch02.SymmetricDirichletNeumann.

theorem HCPolySupport.Internal.Ch02.BookCh02.responseSymmetricDirichletNeumannTheory_of_isEllipticFieldOn {d : ℕ} [NeZero d] (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) (ha : IsSymmetricCoeffField a.toCoeffField) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) : Book.Ch02.ResponseSymmetricDirichletNeumannTheory U a hsym

theorem HCPolySupport.Internal.Ch02.BookCh02.responseSymmetricDirichletNeumannTheory_of_neZero {d : ℕ} [NeZero d] (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Book.Ch02.ResponseSymmetricDirichletNeumannTheory U a hsym

theorem HCPolySupport.Internal.Ch02.BookCh02.responseSymmetricDirichletNeumannTheory {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Book.Ch02.ResponseSymmetricDirichletNeumannTheory U a hsym