Finite and free modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We provide some instances for finite and free modules.
Main results #
module.free.choose_basis_index.fintype: If a free module is finite, then any basis is finite.module.free.linear_map.free: ifMandNare finite and free, thenM →ₗ[R] Nis free.module.free.linear_map.module.finite: ifMandNare finite and free, thenM →ₗ[R] Nis finite.
@[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] :
If a free module is finite, then any basis is finite.
Equations
- module.free.choose_basis_index.fintype R M = _.dcases_on (λ (h : ⊤.fg), (λ (_x : submodule.span R ↑(classical.some h) = ⊤), basis_fintype_of_finite_spans ↑(classical.some h) _x (module.free.choose_basis R M)) _)
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]
[finite ι]
(b : basis ι R M) :
module.finite R M
A free module with a basis indexed by a fintype is finite.
@[protected, instance]
def
module.finite.matrix
{R : Type u}
[comm_ring R]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
[finite ι₁]
[finite ι₂] :
module.finite R (matrix ι₁ ι₂ R)