BlockMatrixField #
Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.
theorem
HCPolySupport.Book.Ch02.blockMatrixFieldAlgebraTheory
{d : ℕ}
(U : Domain d)
(a : CoeffOn U)
:
Public Chapter 2 block-matrix field algebra theorem
l.block.matrix.field.basic.definitions.