Finite and free modules

We provide some instances for finite and free modules.

Main results

• Module.Free.ChooseBasisIndex.fintype : If a free module is finite, then any basis is finite.
• Module.Finite.of_basis : A free module with a basis indexed by a Fintype is finite.

noncomputable instance Module.Free.ChooseBasisIndex.fintype (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] : Fintype (Module.Free.ChooseBasisIndex R M)

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

Equations

• Module.Free.ChooseBasisIndex.fintype R M = Fintype.ofFinite (Module.Free.ChooseBasisIndex R M)

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) : Module.Finite R M

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

instance Module.Finite.matrix {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [Finite ι₁] [Finite ι₂] : Module.Finite R (Matrix ι₁ ι₂ M)