FiniteDimensional

📁 Source: Mathlib/Topology/VectorBundle/FiniteDimensional.lean

Statistics

Metric	Count
Definitions FiniteDimensional, FiniteDimensional	2
Theorems finiteDimensional, finrank_eq	2
Total	4

SetRel

Definitions

Name	Category	Theorems
FiniteDimensional 📖	CompData	6 math math: finiteDimensional_or_infiniteDimensional, not_finiteDimensional_iff, finiteDimensional_inv, finiteDimensional_iff, FiniteDimensional.inv, not_infiniteDimensional_iff

VectorBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteDimensional 📖	mathematical	—	FiniteDimensional NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NontriviallyNormedField.toNormedField	—	LinearEquiv.finiteDimensional RingHomInvPair.ids
finrank_eq 📖	mathematical	—	Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	LinearEquiv.finrank_eq RingHomInvPair.ids

(root)

Definitions

Name	Category	Theorems
FiniteDimensional 📖	MathDef	133 math math: Field.FiniteDimensional.of_exists_primitive_element, FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield, AffineBasis.finiteDimensional, FiniteDimensional.of_fact_finrank_eq_two, Subspace.instModuleDualFiniteDimensional, Affine.Simplex.finiteDimensional_direction_altitude, finiteDimensional_vectorSpan_range, LinearEquiv.finiteDimensional, FiniteDimensional.of_fact_finrank_eq_succ, FiniteDimensional.of_surjective, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, finiteDimensional_direction_affineSpan_of_finite, Field.FiniteDimensional.of_finite_intermediateField, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, Complex.instFiniteDimensionalReal, NumberField.instFiniteDimensional, FiniteDimensional.span_of_finite, ContinuousLinearMap.finiteDimensional, FiniteDimensional.trans, VectorBundle.finiteDimensional, IntermediateField.finiteDimensional_right, FiniteDimensional.of_rank_eq_one, IntermediateField.finiteDimensional_iSup_of_finset, Basis.linearEquiv_dual_iff_finiteDimensional, Subspace.finiteDimensional_quot_dualCoannihilator_iff, FiniteDimensional.of_exists_totallyBounded_nhds, FiniteDimensional.finiteDimensional_quotient, finiteDimensional_vectorSpan_image_of_finite, FiniteDimensional.complexToReal, Submodule.finiteDimensional_finset_sup, FiniteDimensional.of_totallyBounded_nhds_zero, FiniteDimensional.of_finrank_pos, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, FDRep.instFiniteDimensionalHom, FiniteDimensional.rclike_to_real, Submodule.finiteDimensional_sup, finiteDimensional_direction_map, FiniteDimensional.of_locallyCompact_manifold, FiniteDimensional.span_finset, finiteDimensional_vectorSpan_of_finite, Collinear.finiteDimensional_direction_affineSpan, finiteDimensional_direction_affineSpan_insert_set, FiniteDimensional.of_rank_eq_zero, FiniteDimensional.of_subalgebra_toSubmodule, FiniteDimensional.of_isCompact_closedBall₀, Coplanar.finiteDimensional_direction_affineSpan, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, finiteDimensional_direction_affineSpan_insert, IsLocalRing.instFiniteDimensionalResidueFieldCotangentSpaceOfIsNoetherianRing, finiteDimensional_direction_affineSpan_range, LinearMap.finiteDimensional', finiteDimensional_vectorSpan_insert_set, NumberField.to_finiteDimensional, finiteDimensional_vectorSpan_singleton, FiniteDimensional.of_finite_basis, Submodule.finiteDimensional_inf_right, instFiniteDimensionalRealComplex, FiniteDimensional.of_isCompact_closedBall, IsGaloisGroup.finiteDimensional, WithAbs.instFiniteDimensional, FiniteDimensional.of_injective, HasCompactMulSupport.eq_one_or_finiteDimensional, functionField_iff, FiniteDimensional.of_locallyCompactSpace, FiniteDimensional.finiteDimensional_self, LinearMap.finiteDimensional, FiniteDimensional.finiteDimensional_pi', HasCompactSupport.eq_zero_or_finiteDimensional, Collinear.finiteDimensional_vectorSpan, IsCyclotomicExtension.finiteDimensional, IntermediateField.finiteDimensional_adjoin, Module.Basis.finiteDimensional_of_finite, FiniteDimensional.finiteDimensional_submodule, FiniteDimensional.of_totallyBounded_nhds, FiniteDimensional.of_fintype_basis, NumberField.finite_of_discr_bdd, Subalgebra.finiteDimensional_toSubmodule, InfiniteGalois.isOpen_iff_finite, FiniteDimensional.finiteDimensional_pi, Coplanar.finiteDimensional_vectorSpan, FiniteDimensional.finiteDimensional_subalgebra, AffineSubspace.finiteDimensional_sup, FiniteDimensional.of_isCompactOperator_id, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, Module.instFiniteDimensionalOfIsReflexive, finiteDimensional_direction_affineSpan_image_of_finite, Polynomial.IsSplittingField.instFiniteDimensionalSplittingField, IntermediateField.exists_lt_finrank_of_infinite_dimensional, IntermediateField.finiteDimensional_left, IntermediateField.finiteDimensional_iSup_of_finite, Matrix.finiteDimensional, FiniteGaloisIntermediateField.finiteDimensional, LinearMap.finiteDimensional_of_surjective, isCompactOperator_id_iff_finiteDimensional, IsGalois.finiteDimensional_of_finite, krullTopology_mem_nhds_one_iff, Projectivization.instFiniteDimensionalSubtypeMemSubmoduleSubmodule, Submodule.fg_iff_finiteDimensional, krullTopology_mem_nhds_one_iff_of_normal, finiteDimensional_bot, IntermediateField.adjoin.finiteDimensional, MulOpposite.instFiniteDimensional, CSA.fin_dim, WithAbs.instFiniteDimensional_1, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, Ideal.Factors.finiteDimensional_quotient_pow, FiniteDimensional.instSubtypeMemSubmoduleMap, FiniteDimensional.of_finrank_eq_succ, FiniteDimensional.subalgebra_toSubmodule, IntermediateField.finiteDimensional_map, ContinuousLinearMap.finite_dimensional_eigenspace, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, FiniteDimensional.of_rank_eq_nat, MontelSpace.finiteDimensional_of_normedSpace, Submodule.finiteDimensional_of_le, finiteDimensional_direction_affineSpan_singleton, IntermediateField.finiteDimensional_adjoin_pair, instFiniteDimensionalFractionRingOfFinite, MvPolynomial.instFiniteDimensionalROfFinite, IntermediateField.finiteDimensional_iSup_of_finset', normalClosure.is_finiteDimensional, IntermediateField.finiteDimensional_sup, LinearMap.finiteDimensional_range, IsCompactOperator.finiteDimensional, Submodule.finiteDimensional_inf_left, finiteDimensional_finsupp, Module.finiteDimensional_iff_of_rank_eq_nsmul, finiteDimensional_vectorSpan_insert, FiniteDimensional.span_singleton, Polynomial.IsSplittingField.finiteDimensional, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal, Submodule.finiteDimensional_iSup

---

← Back to Index