matrix — Mathlib

English

Given a set S, S.matrix consists of exactly those matrices whose entries all lie in S.

Русский

Для множества S множество S.matrix состоит ровно из тех матриц, чьи элементы все принадлежат S.

LaTeX

$$$\\mathrm{Set}.matrix(S) = \\{M : Matrix m n \\;\\mid\\; \\forall i,j, M_{ij} \\in S\\}$$$

Lean4

/-- Given a set `S`, `S.matrix` is the set of matrices `M`
all of whose entries `M i j` belong to `S`. -/
def matrix (S : Set α) : Set (Matrix m n α) :=
  {M | ∀ i j, M i j ∈ S}

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