Finite modules and types with finitely many elements

This file relates Module.Finite and _root_.Finite.

theorem Submodule.fg_iff_exists_fin_linearMap (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : N.FG ↔ ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), LinearMap.range f = N

theorem Module.Finite.exists_fin' (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Function.Surjective ⇑f

A finite module admits a surjective linear map from a finite free module.

theorem Module.Finite.exists_fin_quot_equiv (R : Type u_3) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (S : Submodule R (Fin n → R)), Nonempty (((Fin n → R) ⧸ S) ≃ₗ[R] M)

A finite module can be realised as a quotient of Fin n → R (i.e. R^n).

theorem Module.finite_of_finite (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] [Module.Finite R M] : Finite M

theorem Module.finite_iff_finite {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] : Module.Finite R M ↔ Finite M

A module over a finite ring has finite dimension iff it is finite.

theorem Set.Finite.submoduleSpan (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] {s : Set M} (hs : s.Finite) : (↑(Submodule.span R s)).Finite

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

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

theorem Module.not_finite_of_infinite_basis {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {ι : Type u_3} [Infinite ι] (b : Basis ι R M) : ¬Module.Finite R M