Defs

📁 Source: Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean

Statistics

Metric	Count
Definitions fintypeBasisIndex, instFintypeElemOfVectorSpaceIndex	2
Theorems finiteDimensional_pi, finiteDimensional_pi', finiteDimensional_quotient, finiteDimensional_self, finiteDimensional_submodule, instSubtypeMemSubmoduleMap, of_fact_finrank_eq_succ, of_fact_finrank_eq_two, of_finite_basis, of_finrank_eq_succ, of_finrank_pos, of_fintype_basis, of_injective, of_surjective, span_finset, span_of_finite, span_singleton, trans, finiteDimensional, finiteDimensional_of_finite, finiteDimensional_iff_of_rank_eq_nsmul, finrank_eq_card_basis', finrank_eq_rank', finrank_of_infinite_dimensional, fg_iff_finiteDimensional	25
Total	27

FiniteDimensional

Definitions

Name	Category	Theorems
fintypeBasisIndex 📖	CompOp	—
instFintypeElemOfVectorSpaceIndex 📖	CompOp	1 math math: FGModuleCat.FGModuleCatCoevaluation_apply_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDimensional_pi 📖	mathematical	—	FiniteDimensional Pi.addCommGroup Ring.toAddCommGroup DivisionRing.toRing Pi.Function.module DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Semiring.toModule	—	Module.Finite.pi Module.Finite.self
finiteDimensional_pi' 📖	mathematical	FiniteDimensional	Pi.addCommGroup Pi.module DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	Module.Finite.pi
finiteDimensional_quotient 📖	mathematical	—	FiniteDimensional HasQuotient.Quotient Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient DivisionRing.toRing Submodule.Quotient.addCommGroup Submodule.Quotient.module	—	Module.Finite.quotient IsScalarTower.left
finiteDimensional_self 📖	mathematical	—	FiniteDimensional Ring.toAddCommGroup DivisionRing.toRing Semiring.toModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	—	Module.Finite.self
finiteDimensional_submodule 📖	mathematical	—	FiniteDimensional Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommGroup DivisionRing.toRing Submodule.module	—	Module.IsNoetherian.finite isNoetherian_submodule' isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing
instSubtypeMemSubmoduleMap 📖	mathematical	—	FiniteDimensional Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Submodule.addCommGroup DivisionRing.toRing Submodule.module	—	Module.Finite.map
of_fact_finrank_eq_succ 📖	mathematical	—	FiniteDimensional	—	of_finrank_eq_succ Fact.out
of_fact_finrank_eq_two 📖	mathematical	—	FiniteDimensional	—	of_fact_finrank_eq_succ
of_finite_basis 📖	mathematical	—	FiniteDimensional	—	Module.Basis.finiteDimensional_of_finite Finite.of_fintype
of_finrank_eq_succ 📖	mathematical	Module.finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	FiniteDimensional	—	Module.finite_of_finrank_eq_succ IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Module.Free.of_divisionRing
of_finrank_pos 📖	mathematical	Module.finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	FiniteDimensional	—	Module.finite_of_finrank_pos IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Module.Free.of_divisionRing
of_fintype_basis 📖	mathematical	—	FiniteDimensional	—	Module.Basis.finiteDimensional_of_finite
of_injective 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	FiniteDimensional	—	Module.Finite.of_injective isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing
of_surjective 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	FiniteDimensional	—	Module.Finite.of_surjective RingHomSurjective.ids
span_finset 📖	mathematical	—	FiniteDimensional Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span SetLike.coe Finset Finset.instSetLike Submodule.addCommGroup DivisionRing.toRing Submodule.module	—	Module.Finite.span_finset
span_of_finite 📖	mathematical	—	FiniteDimensional Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Submodule.addCommGroup DivisionRing.toRing Submodule.module	—	Module.Finite.span_of_finite
span_singleton 📖	mathematical	—	FiniteDimensional Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set Set.instSingletonSet Submodule.addCommGroup DivisionRing.toRing Submodule.module	—	Module.Finite.span_singleton
trans 📖	mathematical	—	FiniteDimensional	—	Module.Finite.trans

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDimensional 📖	mathematical	—	FiniteDimensional	—	RingHomInvPair.ids Module.Finite.equiv

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDimensional_iff_of_rank_eq_nsmul 📖	mathematical	rank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Cardinal AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring	FiniteDimensional	—	finite_iff_of_rank_eq_nsmul IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Free.of_divisionRing
finrank_eq_card_basis' 📖	mathematical	—	Cardinal Cardinal.instNatCast finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	mk_finrank_eq_card_basis IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing
finrank_eq_rank' 📖	mathematical	—	Cardinal Cardinal.instNatCast finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid rank	—	finrank_eq_rank IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing
finrank_of_infinite_dimensional 📖	mathematical	FiniteDimensional	finrank DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	finrank_of_not_finite IsNoetherianRing.strongRankCondition IsSimpleRing.instNontrivial DivisionRing.isSimpleRing PrincipalIdealRing.isNoetherianRing DivisionSemiring.isPrincipalIdealRing Free.of_divisionRing

Module.Basis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDimensional_of_finite 📖	mathematical	—	FiniteDimensional	—	Module.Finite.of_basis

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_iff_finiteDimensional 📖	mathematical	—	FG DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid FiniteDimensional Submodule SetLike.instMembership setLike addCommGroup DivisionRing.toRing module	—	Module.Finite.iff_fg

---

← Back to Index