toSquareBlockProp — Mathlib

English

The square block propagation for M and p is the same as applying toBlock to M with p for both row and column indices.

Русский

Универсальная блочная пропагация для кубической матрицы: toSquareBlockProp(M,p) равняется toBlock(M,p,p).

LaTeX

$$$ \\text{toSquareBlockProp }(M,p) = \\text{toBlock }(M,\\,p,\\,p) $$$

Lean4

/-- Let `p` pick out certain rows and columns of a square matrix `M`. Then
  `toSquareBlockProp M p` is the corresponding block matrix. -/
def toSquareBlockProp (M : Matrix m m α) (p : m → Prop) : Matrix { a // p a } { a // p a } α :=
  toBlock M _ _

Похожие утверждения