FiniteDimensional

📁 Source: Mathlib/Topology/Algebra/SeparationQuotient/FiniteDimensional.lean

Statistics

Metric	Count
Definitions FiniteDimensional, FiniteDimensional, FiniteDimensional	3
Theorems instModuleFinite	1
Total	4

SeparationQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instModuleFinite 📖	mathematical	—	Module.Finite SeparationQuotient instAddCommMonoid instModule	—	Module.Finite.of_surjective RingHomSurjective.ids Quotient.mk_surjective

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

Topology.RelCWComplex

Definitions

Name	Category	Theorems
FiniteDimensional 📖	CompData	2 math math: Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional, Finite.toFiniteDimensional

(root)

Definitions

Name	Category	Theorems
FiniteDimensional 📖	MathDef	118 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, LinearMap.finiteDimensional_of_det_ne_one, 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, IntermediateField.finiteDimensional_right, FiniteDimensional.of_rank_eq_one, Basis.linearEquiv_dual_iff_finiteDimensional, Subspace.finiteDimensional_quot_dualCoannihilator_iff, FiniteDimensional.finiteDimensional_quotient, finiteDimensional_vectorSpan_image_of_finite, FiniteDimensional.complexToReal, 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, FDRep.instFiniteDimensionalCarrierVFGModuleCat, 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, 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, HasCompactSupport.eq_zero_or_finiteDimensional, Collinear.finiteDimensional_vectorSpan, IsCyclotomicExtension.finiteDimensional, IntermediateField.finiteDimensional_adjoin, Module.Basis.finiteDimensional_of_finite, FiniteDimensional.finiteDimensional_submodule, 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, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, Module.instFiniteDimensionalOfIsReflexive, finiteDimensional_direction_affineSpan_image_of_finite, Polynomial.IsSplittingField.instFiniteDimensionalSplittingField, IntermediateField.finiteDimensional_left, Matrix.finiteDimensional, FiniteGaloisIntermediateField.finiteDimensional, LinearMap.finiteDimensional_of_surjective, 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, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, Ideal.Factors.finiteDimensional_quotient_pow, FiniteDimensional.instSubtypeMemSubmoduleMap, FiniteDimensional.of_finrank_eq_succ, FiniteDimensional.subalgebra_toSubmodule, IntermediateField.finiteDimensional_map, 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, normalClosure.is_finiteDimensional, IntermediateField.finiteDimensional_sup, LinearMap.finiteDimensional_range, 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

---

← Back to Index