Finiteness

📁 Source: Mathlib/FieldTheory/Finiteness.lean

Statistics

Metric	Count
Definitions finsetBasis, finsetBasisIndex, fintypeBasisIndex, instFintypeElemOfVectorSpaceIndex	4
Theorems coeSort_finsetBasisIndex, coe_finsetBasisIndex, finite_basis_index, iff_fg, iff_rank_lt_aleph0, range_finsetBasis, card_eq_pow_finrank, natCard_eq_pow_finrank	8
Total	12

IsNoetherian

Definitions

Name	Category	Theorems
finsetBasis 📖	CompOp	1 math math: range_finsetBasis
finsetBasisIndex 📖	CompOp	3 math math: range_finsetBasis, coe_finsetBasisIndex, coeSort_finsetBasisIndex
fintypeBasisIndex 📖	CompOp	—
instFintypeElemOfVectorSpaceIndex 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeSort_finsetBasisIndex 📖	mathematical	—	Finset SetLike.instMembership Finset.instSetLike finsetBasisIndex Set.Elem Module.Basis.ofVectorSpaceIndex	—	Set.Finite.coeSort_toFinset
coe_finsetBasisIndex 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike finsetBasisIndex Module.Basis.ofVectorSpaceIndex	—	Set.Finite.coe_toFinset
finite_basis_index 📖	mathematical	—	Set.Finite	—	Module.Basis.finite_index_of_rank_lt_aleph0 IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Module.rank_lt_aleph0 Module.IsNoetherian.finite
iff_fg 📖	mathematical	—	IsNoetherian DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Module.Finite	—	coe_finsetBasisIndex range_finsetBasis Module.Basis.span_eq iff_rank_lt_aleph0 rank_top lt_of_le_of_lt rank_span_le IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Set.Finite.lt_aleph0 Finset.finite_toSet
iff_rank_lt_aleph0 📖	mathematical	—	IsNoetherian DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Module.rank Cardinal.aleph0	—	Module.Basis.mk_eq_rank'' IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Cardinal.lt_aleph0_iff_set_finite LinearIndependent.set_finite_of_isNoetherian Module.Basis.ofVectorSpaceIndex.linearIndependent isNoetherian_of_linearEquiv isNoetherian_of_fg_of_noetherian isNoetherian_of_isNoetherianRing_of_finite Module.Finite.self Set.Finite.coe_toFinset Module.Basis.span_eq Module.Basis.coe_ofVectorSpace Subtype.range_coe
range_finsetBasis 📖	mathematical	—	Set.range Finset SetLike.instMembership Finset.instSetLike finsetBasisIndex DFunLike.coe Module.Basis DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Module.Basis.instFunLike finsetBasis Module.Basis.ofVectorSpaceIndex	—	finsetBasis.eq_1 Module.Basis.range_reindex Module.Basis.range_ofVectorSpace

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_pow_finrank 📖	mathematical	—	Fintype.card Monoid.toNatPow Nat.instMonoid finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing IsNoetherian.finite isNoetherian_of_finite Finite.of_fintype card_fintype finrank_eq_card_basis IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing
natCard_eq_pow_finrank 📖	mathematical	—	Nat.card Monoid.toNatPow Nat.instMonoid finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Nat.card_congr RingHomInvPair.ids Finite.of_fintype Nat.card_fun finrank_eq_nat_card_basis IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing

---

← Back to Index