matrix — Mathlib

English

If the indexing sets are finite, then the matrix object is finite.

Русский

Если индексы конечны, то матрица конечна.

LaTeX

$$$$ \text{Finite}(\mathrm{Matrix}(\iota_1, \iota_2, M)) $$$$

Lean4

instance matrix {R ι₁ ι₂ M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M]
    [_root_.Finite ι₁] [_root_.Finite ι₂] : Module.Finite R (Matrix ι₁ ι₂ M) :=
  by
  cases nonempty_fintype ι₁
  cases nonempty_fintype ι₂
  exact Module.Finite.of_basis <| (Free.chooseBasis _ _).matrix _ _

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