Documentation

Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Finite and free modules #

We provide some instances for finite and free modules.

Main results #

If a free module is finite, then the arbitrary basis is finite.

Equations
theorem Module.Finite.of_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Finite ι] (b : Basis ι R M) :

A free module with a basis indexed by a Fintype is finite.

instance Module.Finite.matrix {R : Type u} [Semiring R] {ι₁ : Type u_1} {ι₂ : Type u_2} [Finite ι₁] [Finite ι₂] :
Module.Finite R (Matrix ι₁ ι₂ R)
Equations
  • =