Theorems · Definition · linear algebra
FiniteDimensional
(K : Type u_1) → (V : Type u_2) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [Module K V] → Prop
FiniteDimensional vector spaces are defined to be finite modules.
Use Module.Basis.finiteDimensional_of_finite to prove finite dimension from another definition.
- Cited by
- 1,854 results in Mathlib
- Foundations
- Depth 45 from the axioms, rests on 388 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- AddCommGroupstatement and proof · cited by 12,871
- DivisionRingstatement and proof · cited by 1,062
- Module.Finiteproof · cited by 1,032
Cited by2,057
Results whose statement or proof uses this declaration.
- LinearMap.adjointstatement and proof · cited by 64
- stdOrthonormalBasisstatement · cited by 60
- SmoothBumpFunction.toFunstatement and proof · cited by 53
- LinearMap.toContinuousLinearMapstatement and proof · cited by 43
- Module.Basis.ofZLatticeBasisstatement and proof · cited by 36
- LieAlgebra.IsKilling.corootstatement and proof · cited by 34
- LieSubalgebra.rootstatement and proof · cited by 34
- FractionalIdeal.dualstatement and proof · cited by 33
- InnerProductSpace.HarmonicContOnClstatement · cited by 32
- SmoothBumpCoveringstatement · cited by 32
- LinearMap.IsSymmetric.eigenvaluesstatement · cited by 31
- FiniteDimensional.completestatement and proof · cited by 29
Showing the 200 most cited of 2,057.