FixedDetMatrix — Mathlib

English

Fix a ring R and a determinant value m. Consider the subset of square matrices of size n with entries in R whose determinant equals m; this forms a natural object, called FixedDetMatrix(m).

Русский

Фиксируем определитель m и рассматриваем подмножество квадратных матриц размера n с элементами из R, детерминант которых равен m; такое множество обозначается FixedDetMatrix(m).

LaTeX

$$$FixedDetMatrix(m) = \{ A \in \mathrm{Mat}_{n}(R) : \det(A) = m \}$.$$

Lean4

/-- The subtype of matrices with fixed determinant `m` -/
def FixedDetMatrix (m : R) :=
  { A : Matrix n n R // A.det = m }

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