instCoeFunMatrixNat — Mathlib

English

A Coxeter matrix can be viewed as a square matrix with natural-number entries.

Русский

Коксетерова матрица может рассматриваться как квадратная матрица с элементами из натуральных чисел.

LaTeX

$$$$ \\forall i,j \\in B:\\ M(i,j) \\in \\mathbb{N}. $$$$

Lean4

/-- A Coxeter matrix can be coerced to a matrix. -/
instance : CoeFun (CoxeterMatrix B) fun _ ↦ (Matrix B B ℕ) :=
  ⟨M⟩

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