Finite modules and types with finitely many elements #
This file relates Module.Finite and _root_.Finite.
theorem
Module.Finite.exists_fin'
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Module.Finite R M]
:
∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Function.Surjective ⇑f
theorem
Module.finite_of_finite
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Finite R]
[Module.Finite R M]
:
Finite M
@[deprecated Module.finite_of_finite]
theorem
FiniteDimensional.finite_of_finite
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Finite R]
[Module.Finite R M]
:
Finite M
Alias of Module.finite_of_finite.
@[deprecated Module.finite_of_finite]
theorem
FiniteDimensional.fintypeOfFintype
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Finite R]
[Module.Finite R M]
:
Finite M
A finite dimensional vector space over a finite field is finite
theorem
Module.finite_iff_finite
{R : Type u_1}
{M : Type u_4}
[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_4}
[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_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Nontrivial R]
{ι : Type u_6}
[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_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Nontrivial R]
{ι : Type u_6}
[Infinite ι]
(b : Basis ι R M)
:
¬Module.Finite R M