mathlib documentation

linear_algebra.free_module.finite.basic

Finite and free modules #

We provide some instances for finite and free modules.

Main results #

source
@[protected, instance]
noncomputable def module.free.choose_basis_index.fintype (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] [module.free R M] [nontrivial R] [module.finite R M] :
fintype (module.free.choose_basis_index R M)

If a free module is finite, then any basis is finite.

Equations
source
@[protected, instance]
def module.free.linear_map.free (R : Type u) (M : Type v) (N : Type w) [comm_ring R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] [nontrivial R] [module.finite R M] [module.finite R N] :
module.free R (M →ₗ[R] N)
source
theorem module.finite.of_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [comm_ring R] [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) :
module.finite R M

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

source
@[protected, instance]
def module.finite.matrix {R : Type u} [comm_ring R] {ι₁ : Type u_1} [fintype ι₁] {ι₂ : Type u_2} [fintype ι₂] :
module.finite R (matrix ι₁ ι₂ R)
source
@[protected, instance]
def module.free.linear_map.module.finite {R : Type u} {M : Type v} (N : Type w) [comm_ring R] [add_comm_group M] [module R M] [module.free R M] [add_comm_group N] [module R N] [module.free R N] [nontrivial R] [module.finite R M] [module.finite R N] :
module.finite R (M →ₗ[R] N)
source
@[protected, instance]
def module.free.add_monoid_hom.module.finite (M : Type v) (N : Type w) [add_comm_group M] [module.finite ℤ M] [module.free ℤ M] [add_comm_group N] [module.finite ℤ N] [module.free ℤ N] :
module.finite ℤ (M →+ N)
source
@[protected, instance]
def module.free.add_monoid_hom.free (M : Type v) (N : Type w) [add_comm_group M] [module.finite ℤ M] [module.free ℤ M] [add_comm_group N] [module.finite ℤ N] [module.free ℤ N] :
module.free ℤ (M →+ N)