Coarse-graining support: Support.Book.Ch02.Theorems.BlockCoarseMatrix

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

theorem HCPolySupport.Book.Ch02.blockCoarseMatrixTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : BlockCoarseMatrixTheory U a

Public Chapter 2 coarse block matrix theorem l.block.coarse.matrices.basic.definitions.