Finite

📁 Source: Mathlib/Topology/CWComplex/Classical/Finite.lean

Statistics

Metric	Count
Definitions Finite, Finite, Finite, mkFinite, mkFiniteType, Finite, mkFinite, mkFiniteType	8
Theorems finiteType_mkFiniteType, finite_mkFinite, mkFiniteType_cell, mkFiniteType_map, mkFinite_cell, mkFinite_map, toFiniteDimensional, toFiniteType, eventually_isEmpty_cell, finite_cell, finiteType_mkFiniteType, finite_cells_of_finite, finite_iff_finite_cells, finite_mkFinite, finite_of_finiteDimensional_finiteType, finite_of_finite_cells, mkFiniteType_cell, mkFiniteType_map, mkFinite_cell, mkFinite_map	20
Total	28

AlgHom

Definitions

Name	Category	Theorems
Finite 📖	MathDef	7 math math: Finite.of_comp_finite, Finite.of_surjective, Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ, MvPolynomial.finite_universalFactorizationMap, exists_finite_inj_algHom_of_fg, Finite.id, Finite.comp

SSet

Definitions

Name	Category	Theorems
Finite 📖	CompData	21 math math: finite_of_isPullback, finite_iSup_iff, stdSimplex.instFiniteToSSetOfSimplex, instFiniteTensorUnit, finite_of_hasDimensionLT, finite_iff_of_iso, instFiniteToSSet, finite_of_mono, instFiniteTensorObj, instFiniteCoprod, finite_of_isColimit, finite_of_epi, prodStdSimplex.instFiniteTensorObjObjSimplexCategoryStdSimplexMk, finite_subcomplex_top_iff, stdSimplex.instFiniteObjSimplexCategory, finite_range, Finite.exists_epi_from_isCardinalPresentable, instFiniteSigmaObjOfFinite, finite_of_iso, instFinitePullback, instFiniteInitial

Topology.CWComplex

Definitions

Name	Category	Theorems
mkFinite 📖	CompOp	3 math math: mkFinite_map, mkFinite_cell, finite_mkFinite
mkFiniteType 📖	CompOp	3 math math: mkFiniteType_cell, finiteType_mkFiniteType, mkFiniteType_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteType_mkFiniteType 📖	mathematical	Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Set.MapsTo Metric.sphere Set.iUnion IsClosed	Topology.RelCWComplex.FiniteType Set Set.instEmptyCollection instRelCWComplex mkFiniteType	—	—
finite_mkFinite 📖	mathematical	Filter.Eventually IsEmpty Filter.atTop Nat.instPreorder Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Set.MapsTo Metric.sphere Set.iUnion	Topology.RelCWComplex.Finite Set Set.instEmptyCollection instRelCWComplex mkFinite	—	—
mkFiniteType_cell 📖	mathematical	Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Set.MapsTo Metric.sphere Set.iUnion IsClosed	cell mkFiniteType	—	—
mkFiniteType_map 📖	mathematical	Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Set.MapsTo Metric.sphere Set.iUnion IsClosed	map mkFiniteType	—	—
mkFinite_cell 📖	mathematical	Filter.Eventually IsEmpty Filter.atTop Nat.instPreorder Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Set.MapsTo Metric.sphere Set.iUnion	cell mkFinite Topology.RelCWComplex.cell Set Set.instEmptyCollection Topology.RelCWComplex.mkFinite isClosed_empty	—	—
mkFinite_map 📖	mathematical	Filter.Eventually IsEmpty Filter.atTop Nat.instPreorder Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Set.MapsTo Metric.sphere Set.iUnion	map mkFinite Topology.RelCWComplex.map Set Set.instEmptyCollection Topology.RelCWComplex.mkFinite isClosed_empty	—	isClosed_empty

Topology.RelCWComplex

Definitions

Name	Category	Theorems
Finite 📖	CompData	6 math math: finite_of_finiteDimensional_finiteType, finite_of_finite_cells, finite_mkFinite, Subcomplex.finite_subcomplex_of_finite, finite_iff_finite_cells, Topology.CWComplex.finite_mkFinite
mkFinite 📖	CompOp	5 math math: Topology.CWComplex.mkFinite_map, Topology.CWComplex.mkFinite_cell, mkFinite_cell, finite_mkFinite, mkFinite_map
mkFiniteType 📖	CompOp	3 math math: mkFiniteType_cell, mkFiniteType_map, finiteType_mkFiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finiteType_mkFiniteType 📖	mathematical	Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Disjoint Set.MapsTo Metric.sphere Set.instUnion Set.iUnion IsClosed	FiniteType mkFiniteType	—	—
finite_cells_of_finite 📖	mathematical	—	Finite cell	—	FiniteDimensional.eventually_isEmpty_cell Finite.toFiniteDimensional FiniteType.finite_cell Finite.toFiniteType instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat IsEmpty.false not_lt Sigma.eta Equiv.finite_iff Finite.instSigma instFiniteSubtypeLtOfLocallyFiniteOrderBot
finite_iff_finite_cells 📖	mathematical	—	Finite Finite cell	—	finite_cells_of_finite finite_of_finite_cells
finite_mkFinite 📖	mathematical	Filter.Eventually IsEmpty Filter.atTop Nat.instPreorder Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Disjoint Set.MapsTo Metric.sphere Set.instUnion Set.iUnion	Finite mkFinite	—	—
finite_of_finiteDimensional_finiteType 📖	mathematical	—	Finite	—	FiniteType.finite_cell
finite_of_finite_cells 📖	mathematical	—	Finite	—	instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat isEmpty_or_nonempty Nat.instCanonicallyOrderedAdd Finset.image_nonempty Finset.univ_nonempty Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.cast_add Nat.cast_one Finset.le_max' Finite.of_injective sigma_mk_injective
mkFiniteType_cell 📖	mathematical	Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Disjoint Set.MapsTo Metric.sphere Set.instUnion Set.iUnion IsClosed	cell mkFiniteType	—	—
mkFiniteType_map 📖	mathematical	Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Disjoint Set.MapsTo Metric.sphere Set.instUnion Set.iUnion IsClosed	map mkFiniteType	—	—
mkFinite_cell 📖	mathematical	Filter.Eventually IsEmpty Filter.atTop Nat.instPreorder Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Disjoint Set.MapsTo Metric.sphere Set.instUnion Set.iUnion	cell mkFinite	—	—
mkFinite_map 📖	mathematical	Filter.Eventually IsEmpty Filter.atTop Nat.instPreorder Finite PartialEquiv.source Metric.ball pseudoMetricSpacePi Real Fin.fintype Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne ContinuousOn Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace PartialEquiv.toFun Metric.closedBall PartialEquiv.symm PartialEquiv.target Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.univ Set.image Disjoint Set.MapsTo Metric.sphere Set.instUnion Set.iUnion	map mkFinite	—	—

Topology.RelCWComplex.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toFiniteDimensional 📖	mathematical	—	Topology.RelCWComplex.FiniteDimensional	—	—
toFiniteType 📖	mathematical	—	Topology.RelCWComplex.FiniteType	—	—

Topology.RelCWComplex.FiniteDimensional

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_isEmpty_cell 📖	mathematical	—	Filter.Eventually IsEmpty Topology.RelCWComplex.cell Filter.atTop Nat.instPreorder	—	—

Topology.RelCWComplex.FiniteType

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_cell 📖	mathematical	—	Finite Topology.RelCWComplex.cell	—	—

(root)

Definitions

Name	Category	Theorems
Finite 📖	CompData	673 math math: CategoryTheory.ShortComplex.ShortExact.ab_finite_iff, Condensed.finYoneda_obj, TemperedDistribution.lineDerivOpCLM_eq, MeasureTheory.Lp.toTemperedDistributionCLM_apply, Finite.psum_right, TemperedDistribution.fourierInv_toTemperedDistributionCLM_eq, CategoryTheory.PreGaloisCategory.instT2SpaceAutFunctorFintypeCat, Subgroup.instFiniteSubtypeMem, CategoryTheory.PreGaloisCategory.mulAction_def, Matrix.instFinite, FiniteAddGrp.instFiniteCarrierToAddGrp, LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, Distribution.dsupport_delta, Field.finite_intermediateField_of_exists_primitive_element, CategoryTheory.PreGaloisCategory.action_ext_of_isGalois, IsKleinFour.instFinite, Quot.finite, CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsColimitsOfShapeFintypeCatDiscretePEmpty, PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero, SSet.Subcomplex.Pairing.instFiniteSubtypeElemNIIAncestralRel, WellFoundedLT.finite_of_iSupIndep, Quotient.finite, List.Vector.finite, CategoryTheory.PreGaloisCategory.instContinuousSMulAutFintypeCatObjObjFinite, CategoryTheory.instFiniteArrowDiscrete, PrimeSpectrum.finite_of_toPiLocalization_surjective, Profinite.Extend.cocone_pt, CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso, Finite.Set.subset, Finite.Set.finite_image, CategoryTheory.Limits.FintypeCat.hasFiniteColimits, MeasurableSpace.instFinite_countablePartition, Finite.of_equiv, AddCommGrpCat.prop_isFinite_iff, FintypeCat.instFiniteIso, instFullFintypeCatProfiniteToProfinite, CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsLimitsOfShapeFintypeCatDiscretePEmpty, Profinite.Extend.functorOp_map, ENat.card_lt_top, CategoryTheory.PreGaloisCategory.instFiniteAutOfIsConnected, QuotientGroup.finite, CategoryTheory.PreGaloisCategory.endEquivSectionsFibers_π, CategoryTheory.FintypeCat.Action.pretransitive_of_isConnected, FintypeCat.uSwitch_map_uSwitch_map, FintypeCat.instFaithfulIncl, CategoryTheory.PreGaloisCategory.autEmbedding_injective, Set.FiniteExhaustion.instFiniteElemCoeNat, FirstOrder.Language.empty.isFraisse_finite, CategoryTheory.PreGaloisCategory.instContinuousMulAutFunctorFintypeCat, CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget, TemperedDistribution.fourierMultiplierCLM_smul, Finite.Set.finite_of_finite_image, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, FirstOrder.Language.Structure.fg_iff_finite, TemperedDistribution.lineDerivOp_fourier_eq, PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, LightCondensed.finYoneda_obj, LightCondensed.isoFinYoneda_inv_app, IsSimpleGroup.finite, finite_of_compact_of_discrete, CategoryTheory.Mat.equivalenceSingleObjInverse_obj_obj, FunctorToFintypeCat.naturality, CategoryTheory.PreGaloisCategory.toAutMulEquiv_isHomeomorph, Profinite.Extend.cone_π_app, TemperedDistribution.smulLeftCLM_compL_smulLeftCLM, SimplexCategory.instFiniteHom, Set.Finite.finite_of_compl, IsLocalRing.ResidueField.finite_of_finite, instFaithfulFintypeCatLightProfiniteToLightProfinite, CategoryTheory.PreGaloisCategory.FiberFunctor.reflectsIsos, LightCondensed.finYoneda_map, CategoryTheory.PreGaloisCategory.initial_iff_fiber_empty, LieModule.Weight.instFinite, instFiniteProp, CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesColimitsOfShapeFintypeCatSingleObjOfFinite, CategoryTheory.PreGaloisCategory.FiberFunctor.instPreservesFiniteLimitsFintypeCat, instFiniteAbelianization, SimpleGraph.instFinite, instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal, CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan, PointwiseConvergenceCLM.continuous_of_continuous_eval, Distribution.IsVanishingOn.smulLeftCLM, AddAction.finite_quotient_of_finite_quotient_of_finite_quotient, CategoryTheory.PreGaloisCategory.card_aut_le_card_fiber_of_connected, TemperedDistribution.fourierMultiplierCLM_compL_fourierMultiplierCLM, PointwiseConvergenceCLM.tendsto_nhds, FintypeCat.equivEquivIso_apply_hom, FintypeCat.instFiniteHom, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesQuotientsByFiniteGroups, MaximalSpectrum.finite_of_toPiLocalization_surjective, CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsMonomorphismsFintypeCat, AddGroup.fg_iff_exists_freeAddGroup_hom_surjective_finite, Finite.algHom, FiniteGrp.isFinite, not_finite_iff_infinite, CategoryTheory.PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat, MulEquiv.finite_left, AddSubgroup.quotient_finite_of_isOpen', CategoryTheory.FintypeCat.instFiberFunctorActionFintypeCatForget₂HomSubtypeHomObjFiniteV, Finite.Set.finite_diff, WellFoundedGT.finite_of_iSupIndep, Polynomial.IsSplittingField.instFiniteSplittingField, TemperedDistribution.smulLeftCLM_neg, LightProfinite.Extend.cocone_ι_app, PointwiseConvergenceCLM.postcomp_apply, CategoryTheory.GradedObject.instFiniteElemProdNatPreimageHAddFstSndSingletonSet, Function.HasTemperateGrowth.toTemperedDistribution_apply, Condensed.lanPresheafExt_inv, CategoryTheory.ShortComplex.Exact.ab_finite, instFiniteSubtypeLtOfLocallyFiniteOrderTop, finite_iff_subgroup_quotient, CategoryTheory.FintypeCat.instHasColimitsOfShapeSingleObjFintypeCatOfFinite, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContActionOfFiberFunctor, Finite.Set.finite_insert, Set.finite_range_iff, CategoryTheory.PreGaloisCategory.card_fiber_coprod_eq_sum, TemperedDistribution.instLineDerivLeftSMulReal, instFaithfulFintypeCatProfiniteToProfinite, CategoryTheory.GradedObject.instFiniteElemProdNatSetOfEqHAddFstSnd, instFinitePLift, Subtype.finite, TemperedDistribution.fourierInv_lineDerivOp_eq, Finite.Set.finite_sUnion, FirstOrder.Language.dlo_age, Pi.finite, Matrix.SpecialLinearGroup.instFinite, CategoryTheory.PreGaloisCategory.connected_component_unique, TemperedDistribution.instFourierAdd, TemperedDistribution.laplacian_eq_fourierMultiplierCLM, Finite.Set.finite_sep, lightDiagramToLightProfinite_obj, Finite.Set.finite_seq, PointwiseConvergenceCLM.instLocallyConvexSpace, FirstOrder.Language.Structure.FG.finite, FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite, TemperedDistribution.instFourierSMul, CategoryTheory.PreGaloisCategory.instFullContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, Profinite.Extend.functorOp_obj, TemperedDistribution.delta_apply, Fintype.finite, Condensed.finYoneda_map, instFiniteCarrierToTopTotallyDisconnectedSpaceOfObj, Equiv.finite_iff, RegularWreathProduct.instFinite, Subgroup.finite_quotient_of_finiteIndex, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family, TemperedDistribution.instContinuousFourier, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesPullbacks, CategoryTheory.PreGaloisCategory.toAut_hom_app_apply, Subgroup.finite_iff_finite_and_finiteIndex, FintypeCat.toProfinite_map_hom_hom_apply, instFiniteCuspOrbitsOfIsArithmetic, FunLike.finite, Finite.of_ideal_quotient, CategoryTheory.Limits.FintypeCat.productEquiv_apply, CategoryTheory.PreGaloisCategory.obj_discreteTopology, FintypeCat.comp_apply, Finite.Set.finite_range, FintypeCat.uSwitchEquiv_naturality, Finite.of_forall_not_lt_lt, FintypeCat.comp_hom, CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction, FintypeCat.equivEquivIso_symm_apply_symm_apply, CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected, CategoryTheory.Limits.FintypeCat.hasFiniteLimits, LinearIndependent.finite_of_le_span_finite, CategoryTheory.FintypeCat.instMonoActionFintypeCatImageComplementIncl, IsArtinianRing.finite_of_compactSpace_of_t2Space, QuotientAddGroup.finite, instFiniteMonoidHomUnits, SchwartzMap.delta_apply, Finite.Set.finite_image2, CategoryTheory.PreGaloisCategory.instEssSurjContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, FintypeCat.incl_map, FintypeCat.hom_ext_iff, SSet.instFiniteElemObjOppositeSimplexCategoryOpMkNonDegenerateOfFinite, CategoryTheory.Subfunctor.IsFinite.instFiniteIndex, PointwiseConvergenceCLM.instT2Space, CategoryTheory.Limits.FintypeCat.finite_colimitType, AlgebraicGeometry.QuasiCompactCover.exists_hom, FintypeCat.Skeleton.instIsEquivalenceIncl, CategoryTheory.PreGaloisCategory.autIsoFibers_inv_app, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.transitive_of_isGalois, Submodule.fg_iff_exists_finite_generating_family, Ideal.instFinite, finite_iff_addSubgroup_quotient, FintypeCat.id_apply, finite_or_infinite, CategoryTheory.PreGaloisCategory.functorToContAction_map, Subgroup.IsComplement.finite_right_iff, AddSubgroup.finite_quotient_of_pretransitive_of_index_ne_zero, CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringRight, Submodule.finiteQuotient_iff, CategoryTheory.PreGaloisCategory.nonempty_fiber_of_isConnected, CategoryTheory.Limits.FintypeCat.productEquiv_symm_comp_π_apply, PointwiseConvergenceCLM.isEmbedding_coeFn, SheafOfModules.GeneratingSections.IsFiniteType.finite, Configuration.instFiniteDual, Matrix.instFiniteSpectrum, CategoryTheory.PreGaloisCategory.instPreservesIsConnectedActionFintypeCatAutFunctorFunctorToAction, AlgebraicGeometry.IsArtinianScheme.finite, Finite.of_finite_quot_finite_addSubgroup, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, hasCardinalLT_aleph0_iff, DFunLike.finite, HahnSeries.SummableFamily.finite_co_support_prod_smul, Sylow.instFiniteQuotientSubgroupNormalizer, CStarMatrix.instFinite, SSet.instFiniteObjOppositeSimplexCategoryTensorObj, PointwiseConvergenceCLM.isInducing_inducingFn, FiniteGrp.instFiniteCarrierToGrp, Finite.Set.finite_iUnion, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_fst_apply, Finite.of_injective_finite_range, TemperedDistribution.fourierMultiplierCLM_apply, Finite.Set.finite_inter_of_right, CategoryTheory.PreGaloisCategory.toAutHomeo_apply, Sylow.finite_of_finiteIndex, CategoryTheory.PreGaloisCategory.exists_set_ker_evaluation_subset_of_isOpen, TemperedDistribution.fourier_toTemperedDistributionCLM_eq, Ideal.absNorm_ne_zero_iff, Finite.Set.finite_union, SSet.instFiniteObjOppositeSimplexCategoryOfFinite, CategoryTheory.PreGaloisCategory.exists_lift_of_continuous, TopologicalSpace.Clopens.finite_prod, TemperedDistribution.fourierMultiplierCLM_const, CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois, CategoryTheory.PreGaloisCategory.instIsPretransitiveObjFiniteObjFintypeCatOfIsConnected, Finite.instProd, Finite.instPProd, FirstOrder.Language.isFraisse_finite_linear_order, IsLocalRing.finite_residueField_of_compactSpace, PointwiseConvergenceCLM.equivWeakDual_apply, CategoryTheory.PreGaloisCategory.instIsPretransitiveAutObjFiniteVFintypeCatFunctorObjActionFunctorToActionOfIsGalois, CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply, Action.FintypeCat.toEndHom_apply, TemperedDistribution.fourierTransformInv_toTemperedDistributionCLM_eq, Finite.instSigma, FintypeCat.equivEquivIso_apply_inv, CategoryTheory.PreGaloisCategory.toAut_isHomeomorph, IsPrimitiveRoot.finite_quotient_span_sub_one', Finite.sum_left, SimpleGraph.ConnectedComponent.instFinite, SchwartzMap.toTemperedDistributionCLM_apply_apply, instFiniteIteratedWreathProduct, Projectivization.finite_of_finite, CategoryTheory.PreGaloisCategory.lt_card_fiber_of_mono_of_notIso, TemperedDistribution.smulLeftCLM_sub, IsPrimitiveRoot.finite_quotient_span_sub_one, Finite.of_subgroup_quotient, Condensed.isColimitLocallyConstantPresheaf_desc_apply, instFiniteObjOpenNormalSubgroupStabilizerHomSurjectiveAuxFunctor, FintypeCatDiscrete.instDiscreteTopologyObjFinite, CategoryTheory.PreGaloisCategory.exists_lift_of_mono_of_isConnected, IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace, not_infinite_iff_finite, CategoryTheory.FintypeCat.instGaloisCategoryActionFintypeCat, PointwiseConvergenceCLM.equivWeakDual_symm_apply, Finite.Set.finite_biUnion', CategoryTheory.PreGaloisCategory.evaluation_aut_bijective_of_isGalois, MulAction.finite_quotient_of_finite_quotient_of_finite_quotient, FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo, Finite.prod_right, CategoryTheory.PreGaloisCategory.nonempty_fiber_pi_of_nonempty_of_finite, Module.finite_iff_finite, LightProfinite.Extend.functor_map, Nat.card_pos_iff, CategoryTheory.PreGaloisCategory.instIsFundamentalGroupAutFunctorFintypeCat, CategoryTheory.PreGaloisCategory.instFiniteHomOfIsConnected, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesTerminalObjects, FintypeCat.isSkeleton, Sylow.finite_of_ker_is_pGroup, AddAction.finite_quotient_of_pretransitive_of_finite_quotient, LightCondensed.isoLocallyConstantOfIsColimit_inv, AddCommGroup.finite_of_fg_torsion, FintypeCat.toLightProfinite_map_hom_hom_apply, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeActionFintypeCatAutFunctorSingleObjFunctorToActionOfFinite, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, IsGaloisGroup.finite, Subgroup.instFiniteSubtypeMemCommutatorOfElemCommutatorSet, CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_symm_app, finite_iff_ideal_quotient, Projectivization.finite_iff_of_finite, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyObjFintypeCatLightProfiniteToLightProfinite, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteObjFinite, instFiniteElemProdCommutatorRepresentatives, Matrix.instFiniteElemRealSpectrum, Submodule.finite_quotient_smul, Condensed.isoLocallyConstantOfIsColimit_inv, CategoryTheory.PreGaloisCategory.FibreFunctor.end_isIso, Finite.of_fintype, FintypeCat.discreteTopology, IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation, AddSubgroup.index_ne_zero_iff_finite, PointwiseConvergenceCLM.coeLMₛₗ_apply, TemperedDistribution.fourierMultiplierCLM_toTemperedDistributionCLM_eq, MulChar.finite, CategoryTheory.PreGaloisCategory.continuousSMul_aut_fiber, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, Condensed.lanPresheafNatIso_hom_app, Set.instFinite, fintypeToFinBoolAlgOp_map, Equiv.finite_left, TemperedDistribution.instLineDerivSMulReal, Finite.of_addSubgroup_quotient, PointwiseConvergenceCLM.continuousEvalConst, instFiniteAdditive, CategoryTheory.coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, MeasureTheory.Measure.toTemperedDistribution_apply, Profinite.Extend.functor_obj, PointwiseConvergenceCLM.coeLM_apply, Equiv.finite_right, Set.Finite.to_subtype, MulAction.finite_quotient_of_pretransitive_of_finite_quotient, FintypeCat.equivEquivIso_symm_apply_apply, SSet.stdSimplex.instFiniteObjOppositeSimplexCategory, CategoryTheory.PreGaloisCategory.FiberFunctor.instFaithfulFintypeCat, TemperedDistribution.fourier_lineDerivOp_eq, Set.finite_coe_iff, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_apply, Action.FintypeCat.quotientToEndHom_mk, TemperedDistribution.lineDerivOp_toTemperedDistributionCLM_eq, CategoryTheory.PreGaloisCategory.FibreFunctor.end_isUnit, CategoryTheory.PreGaloisCategory.aut_discreteTopology, Finite.Set.finite_biUnion'', CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers, CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv_symm_snd_apply, TemperedDistribution.laplacian_eq_sum, CategoryTheory.PreGaloisCategory.card_hom_le_card_fiber_of_connected, Topology.RelCWComplex.FiniteType.finite_cell, instFiniteMaximalSpectrumOfIsFractionRing, Prop.instFinite, instFiniteSym, TemperedDistribution.instContinuousLineDeriv, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, Finite.algEquiv, SimpleGraph.instFiniteEdgeLabelingOfElemSym2EdgeSet, Subgroup.instFiniteQuotientSubtypeMemOpenSubgroupOfIsTopologicalGroupOfCompactSpace, Finite.ofBijective, Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, Distribution.IsVanishingOn.iteratedLineDerivOp, CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.instFiniteSubtypePSingle, AddSubgroup.finite_quotient_of_finite_quotient_of_index_ne_zero, instFiniteMonoidHomUnitsOfHasEnoughRootsOfUnityExponent, CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteLimits, FintypeCat.instIsEquivalenceUSwitch, TopologicalSpace.NoetherianSpace.finite, SetLike.instFinite, FintypeCat.Skeleton.instEssSurjIncl, FintypeCat.homMk_eq_id_iff, Distribution.dsupport_smulLeftCLM_subset, Nat.card_eq, Field.exists_primitive_element_iff_finite_intermediateField, CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective, SimpleGraph.componentCompl_finite, MaximalSpectrum.finite_of_toPiLocalization_pi_surjective, TemperedDistribution.smulLeftCLM_add, LightProfinite.Extend.functorOp_map, HahnSeries.SummableFamily.finite_co_support_prod_mul, basis_finite_of_finite_spans, Subgroup.index_ne_zero_iff_finite, Finite.instSum, CategoryTheory.PreGaloisCategory.functorToAction_map, PointwiseConvergenceCLM.precomp_apply, AddSubgroup.finite_quotient_of_finiteIndex, Submodule.finiteQuotientOfFreeOfRankEq, Finite.instPSum, CategoryTheory.PreGaloisCategory.fiber_in_connected_component, TopologicalSpace.Fiber.instFiniteFiberCoeLocallyConstant, TemperedDistribution.fourierTransform_apply, Subgroup.finiteIndex_iff_finite_quotient, FintypeCat.comp_hom_assoc, instFiniteMultiplicative, finite_of_span_finite_eq_top_finsupp, CategoryTheory.Functor.toEventualRanges_finite, CategoryTheory.instFiniteDiscrete, Module.finite_finsupp_iff, AddSubgroup.finite_iff_finite_and_finiteIndex, FintypeCat.instFullForgetHomObjFinite, CategoryTheory.Limits.FintypeCat.instPreservesFiniteLimitsFintypeCatForgetHomObjFinite, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_fst_apply, CategoryTheory.PreGaloisCategory.FiberFunctor.comp_right, instFiniteULift, CategoryTheory.FintypeCat.Action.isConnected_iff_transitive, Group.fg_iff_exists_freeGroup_hom_surjective_finite, Topology.RelCWComplex.finite_cells_of_finite, FintypeCat.instFullIncl, Cardinal.lt_aleph0_iff_finite, CategoryTheory.PreGaloisCategory.instPreservesFiniteCoproductsActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.PreGaloisCategory.exists_hom_from_galois_of_fiber, Finite.of_subsingleton, Subgroup.quotient_finite_of_isOpen', FintypeCat.hom_apply, CategoryTheory.PreGaloisCategory.autMulEquivAutGalois_π, CategoryTheory.Functor.toPreimages_finite, DiscreteQuotient.instFiniteQuotientOfCompactSpace, CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply, CategoryTheory.PreGaloisCategory.surjective_on_fiber_of_epi, Subgroup.finite_quotient_of_pretransitive_of_index_ne_zero, Filter.cofinite_eq_bot_iff, CategoryTheory.Mat.comp_apply, CategoryTheory.Limits.FintypeCat.finite_of_isColimit, CategoryTheory.PreGaloisCategory.IsFundamentalGroup.continuous_smul, FintypeCat.Skeleton.instFullIncl, Finite.of_finite_addAction_orbitRel_quotient, finite_of_fin_dim_affineIndependent, FiniteAddGrp.isFinite, FintypeCat.Skeleton.incl_mk_nat_card, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesFiniteCoproducts, CategoryTheory.PreGaloisCategory.instPreservesColimitsOfShapeFintypeCatSingleObjInclOfFinite, CategoryTheory.PreGaloisCategory.endEquivAutGalois_mul, CategoryTheory.PreGaloisCategory.isGalois_iff_pretransitive, instFiniteZModUnits, instFiniteElemSubtypeMemSubgroupClosureCommutatorRepresentativesCommutatorSet, finite_iff_nonempty_fintype, DoubleCoset.finite_quotient_iff_exists_finset_iUnion_eq_univ, FirstOrder.Language.Substructure.FG.finite, IsLocalization.finite, TemperedDistribution.fourierMultiplierCLM_apply_apply, Profinite.Extend.functorOp_final, instFiniteUnits, instFiniteWithTop, CategoryTheory.PreGaloisCategory.instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction, CategoryTheory.PreGaloisCategory.comp_autMap_apply, CategoryTheory.PreGaloisCategory.not_initial_iff_fiber_nonempty, TemperedDistribution.instFourierInvSMul, CategoryTheory.PreGaloisCategory.has_decomp_quotients, LightCondensed.lanPresheafNatIso_hom_app, Distribution.dsupport_iteratedLineDerivOp_subset, Algebra.FormallyEtale.iff_exists_algEquiv_prod, TemperedDistribution.instFourierInvAdd, CategoryTheory.Subfunctor.IsFinite.exists_isGeneratedBy, CategoryTheory.PreGaloisCategory.autEmbedding_apply, AddSubgroup.instFiniteSubtypeMem, TemperedDistribution.fourierInv_apply, CategoryTheory.Limits.FintypeCat.instHasLimitsOfShapeFintypeCatOfFinCategory, Action.FintypeCat.quotientToQuotientOfLE_hom_mk, Finite.of_finite_mulAction_orbitRel_quotient, PointwiseConvergenceCLM.tendsto_nhds_atTop, TemperedDistribution.fourierTransform_toTemperedDistributionCLM_eq, LightProfinite.Extend.cocone_pt, instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian, TemperedDistribution.instLineDerivAdd, Function.Embedding.finite, CategoryTheory.PreGaloisCategory.stabilizer_normal_of_isGalois, OrderDual.finite, TopologicalSpace.Opens.instFinite, FintypeCat.inv_hom_id_apply, FintypeCat.instFiniteObj, TemperedDistribution.instLineDerivSMulComplex, Module.finite_of_fg_torsion, CategoryTheory.PreGaloisCategory.instReflectsIsomorphismsActionFintypeCatAutFunctorFunctorToAction, AddMonoidHom.finite_iff_finite_ker_range, Finite.Set.finite_inter_of_left, Ideal.finite_quotient_pow, Profinite.Extend.cocone_ι_app, CategoryTheory.PreGaloisCategory.evaluation_aut_surjective_of_isGalois, Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, TemperedDistribution.laplacian_toTemperedDistributionCLM_eq, instFiniteCarrierToTopTotallyDisconnectedSpaceObjFintypeCatProfiniteToProfinite, IsSimpleAddGroup.finite, Set.FiniteExhaustion.finite', MonoidHom.finite_iff_finite_ker_range, CategoryTheory.Mat.comp_def, Distribution.dsupport_lineDerivOp_subset, Algebra.IsStandardSmooth.out, CategoryTheory.PreGaloisCategory.PointedGaloisObject.Hom.comp, CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois_symm_fiber, SimpleGraph.Subgraph.instFinite, Condensed.isoFinYoneda_hom_app, TemperedDistribution.fourierMultiplierCLM_sum, PointwiseConvergenceCLM.tendsto_iff_forall_tendsto, instFiniteWithBot, CategoryTheory.PreGaloisCategory.autEmbedding_range, Profinite.Extend.cone_pt, lightDiagramToLightProfinite_map, SimpleGraph.componentComplFunctor_finite, CategoryTheory.Mat.id_apply, CategoryTheory.PreGaloisCategory.surjective_of_nonempty_fiber_of_isConnected, NonUnitalRingHom.finite_srange, CategoryTheory.PreGaloisCategory.mulAction_naturality, IsArtinianRing.instFinitePrimeSpectrum, LightCondensed.lanPresheafExt_inv, Condensed.lanPresheafExt_hom, TemperedDistribution.derivCLM_toTemperedDistributionCLM_eq, Finite.Set.finite_replacement, Monoid.fg_iff_exists_freeGroup_hom_surjective_finite, Bool.instFinite, CategoryTheory.Arrow.finite_iff, Ring.HasFiniteQuotients.finiteQuotient, MeasureTheory.Lp.ker_toTemperedDistributionCLM_eq_bot, MeasureTheory.Lp.toTemperedDistribution_toLp_eq, Finite.of_summable_const, CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CategoryTheory.Limits.FintypeCat.jointly_surjective, TemperedDistribution.laplacian_apply_apply, Set.powersetCard.instFiniteElemFinset, TemperedDistribution.smulLeftCLM_smulLeftCLM_apply, Infinite.not_finite, TemperedDistribution.isVanishingOn_delta, Finite.psum_left, Finite.Set.finite_biUnion, PointwiseConvergenceCLM.hasBasis_nhds_zero, CategoryTheory.PreGaloisCategory.exists_lift_of_mono, TemperedDistribution.lineDerivOp_apply_apply, LightProfinite.Extend.functor_initial, TemperedDistribution.lineDerivOp_fourierInv_eq, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, CategoryTheory.PreGaloisCategory.functorToContAction_obj_obj, IsAddKleinFour.instFinite, FintypeCat.uSwitchEquiv_symm_naturality, AddEquiv.finite_left, CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isGalois, Finite.of_finite_quot_finite_ideal, FintypeCat.homMk_eq_comp_iff, CategoryTheory.PreGaloisCategory.instIsEquivalenceContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, CategoryTheory.PreGaloisCategory.endEquivAutGalois_π, Module.finite_finsupp_self_iff, Finite.Set.finite_prod, CategoryTheory.PreGaloisCategory.instIsTopologicalGroupAutFunctorFintypeCat, Nat.card_ne_zero, MeasureTheory.Lp.toTemperedDistribution_apply, TemperedDistribution.smulLeftCLM_const, Subgroup.finite_quotient_of_finite_quotient_of_index_ne_zero, HasEnoughRootsOfUnity.finite_rootsOfUnity, TemperedDistribution.smulLeftCLM_sum, Module.finite_of_finite, CategoryTheory.Precoherent.pullback, Valued.integer.totallyBounded_iff_finite_residueField, AddSubgroup.IsComplement.finite_right_iff, Module.Finite.finite_basis, FintypeCat.hom_inv_id_apply, TemperedDistribution.instContinuousFourierInv, IsSimpleOrder.instFinite, AddSubgroup.finiteIndex_iff_finite_quotient, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, instFiniteZerothHomotopyOfCompactSpace, ModN.instFinite, instFiniteCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyOfObj, CategoryTheory.Presieve.Extensive.arrows_nonempty_isColimit, PointwiseConvergenceCLM.evalCLM_apply, LinearIndependent.finite_of_isNoetherian, Module.finitePresentation_iff_exists_presentation, TemperedDistribution.fourier_apply, SchwartzMap.coe_apply, SheafOfModules.Presentation.IsFinite.finite_relations, IsArtinianRing.instFiniteMaximalSpectrum, CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup, CategoryTheory.FintypeCat.instPreGaloisCategoryActionFintypeCat, CategoryTheory.PreGaloisCategory.fiberEqualizerEquiv_symm_ι_apply, Cardinal.mk_lt_aleph0_iff, Finite.instPSigma, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, Nat.finite_of_card_ne_zero, TemperedDistribution.smulLeftCLM_smul, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, AddSubgroup.quotient_finite_of_isOpen, PointwiseConvergenceCLM.withSeminorms, LinearIndependent.finite, Subgroup.instFiniteQuotientOfSeparatelyContinuousMulOfCompactSpace, instFinite_memPartition, CategoryTheory.PreGaloisCategory.toAut_bijective, CategoryTheory.Limits.FintypeCat.instPreservesFiniteColimitsFintypeCatForgetHomObjFinite, Function.Bijective.finite_iff, TemperedDistribution.derivCLM_apply_apply, AddSubgroup.instFiniteQuotientOfSeparatelyContinuousAddOfCompactSpace, PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis, CategoryTheory.FintypeCat.instPreservesFiniteLimitsActionFintypeCatForgetHomSubtypeHomObjFiniteV, CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, instFiniteConjClasses, Finite.Set.finite_iInter, CategoryTheory.Limits.FintypeCat.instFiniteObjCompFintypeCatIncl, Shrink.instFinite, instFiniteConnectedComponentsOfLocallyConnectedSpaceOfCompactSpace, CategoryTheory.PreGaloisCategory.isPretransitive_of_isGalois, CategoryTheory.PreGaloisCategory.has_decomp_connected_components', CategoryTheory.Arrow.finite, FintypeCat.incl_obj, ContinuousLinearMap.toPointwiseConvergenceCLM_apply, finite_iff_exists_equiv_fin, instFiniteSubtypeLeOfLocallyFiniteOrderBot, PrimeSpectrum.finite_of_toPiLocalization_pi_surjective, Subgroup.IsComplement.finite_left_iff, Algebra.Etale.iff_exists_algEquiv_prod, CategoryTheory.PreGaloisCategory.exists_galois_representative, TemperedDistribution.fourierTransformInv_apply, FintypeCat.id_hom, LightCondensed.lanPresheafExt_hom, CategoryTheory.PreGaloisCategory.PointedGaloisObject.cocone_app, Finite.of_finite_quot_finite_subgroup, CategoryTheory.PreGaloisCategory.instFaithfulContActionFintypeCatHomObjFiniteAutFunctorFunctorToContAction, MulEquiv.finite_right, Condensed.isoFinYoneda_inv_app, PointwiseConvergenceCLM.isUniformEmbedding_coeFn, IsLocalRing.finite_quotient_iff, fintypeToFinBoolAlgOp_obj, CategoryTheory.PreGaloisCategory.instCompactSpaceAutFunctorFintypeCat, CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction, AddMonoid.fg_iff_exists_freeAddGroup_hom_surjective_finite, Subgroup.quotient_finite_of_isOpen, Profinite.Extend.functor_initial, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits, AffineBasis.finite, Ideal.finite_quotient_prod, Topology.RelCWComplex.finite_iff_finite_cells, IsLocalRing.isOpen_iff_finite_quotient, AddEquiv.finite_right, CategoryTheory.PreGaloisCategory.toAut_injective_of_non_trivial, Profinite.Extend.functor_map, Finite.of_not_infinite, CategoryTheory.PreGaloisCategory.has_decomp_connected_components, instFiniteSubtypeLeOfLocallyFiniteOrderTop, CategoryTheory.PreGaloisCategory.endMulEquivAutGalois_pi, Condensed.locallyConstantIsoFinYoneda_hom_app, Set.finite_univ_iff, Algebra.IsStandardSmoothOfRelativeDimension.out, FintypeCat.instFiniteAut, CommGroup.finite_of_fg_torsion, instFullFintypeCatLightProfiniteToLightProfinite, Finite.of_surjective, Ideal.finiteQuotientOfFreeOfNeBot, Finite.prod_left, FintypeCat.homMk_apply, SSet.Finite.finite, CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatOfFinCategory, Distribution.IsVanishingOn.lineDerivOp, FintypeCat.Skeleton.instFaithfulIncl, instFiniteOption, CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected, SimpleGraph.Hom.instFinite, instFiniteSubtypeLtOfLocallyFiniteOrderBot, CategoryTheory.Mat.id_def, Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero, TemperedDistribution.laplacianCLM_apply, hallMatchingsOn.finite, CategoryTheory.PreGaloisCategory.FiberFunctor.preservesEpis, instFiniteQuotientIdealOfIsMaximal, LightProfinite.Extend.functorOp_final, Condensed.lanPresheafIso_hom, IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton, MeasureTheory.Lp.toTemperedDistribution_smul_eq, CategoryTheory.FintypeCat.Action.isConnected_of_transitive, AddSubgroup.IsComplement.finite_left_iff, AddSubgroup.instFiniteQuotientSubtypeMemOpenAddSubgroupOfIsTopologicalAddGroupOfCompactSpace, CategoryTheory.GaloisCategory.hasFiberFunctor, CategoryTheory.PreGaloisCategory.functorToAction_full, Finite.sum_right, CategoryTheory.Limits.FintypeCat.nonempty_pi_of_nonempty, Algebra.QuasiFinite.finite_primeSpectrum, Sylow.finite_of_injective, AlgHom.IsArithFrobAt.finite_quotient, TemperedDistribution.smulLeftCLM_apply_apply, CategoryTheory.PreGaloisCategory.toAut_continuous, CategoryTheory.PreGaloisCategory.autEmbedding_isClosedEmbedding, Profinite.exists_hom, Action.FintypeCat.toEndHom_trivial_of_mem, CategoryTheory.PreGaloisCategory.instContinuousInvAutFunctorFintypeCat, Prod.finite_iff, Finite.of_finite_univ, DivisionRing.finite_of_compactSpace_of_t2Space, Sylow.instFiniteSubtypeMemSubgroup, Action.FintypeCat.ofMulAction_apply, CategoryTheory.PreGaloisCategory.instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction, Finite.of_injective, FirstOrder.Language.Substructure.fg_iff_finite, CategoryTheory.PreGaloisCategory.autEmbedding_range_isClosed, CategoryTheory.PreGaloisCategory.functorToAction_comp_forget₂_eq

---

← Back to Index