Main results

The main results that the formalization.yaml of FormalFrontier/minimal-primes lists under status.main_results at commit 45952e34, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

Declaration	Kind	Where	Note
Order.krullDim_pi_eq_iSup_range_restrict	theorem	MinimalPrimes/Order/KrullDimension.lean, line 823
Order.height_toLex_pi	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1359
Order.coheight_toLex_pi	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1424
Set.chainHeight_biUnion_finset_of_disjoint_of_cross	theorem	MinimalPrimes/Order/ChainHeight.lean, line 659
Order.height_eq_chainHeight_Iio	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1169
Order.coheight_eq_chainHeight_Ioi	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1195
Order.height_toLex_prod	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1205
Order.coheight_toLex_prod	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1250
Order.height_pi_eq_iSup_finset	theorem	MinimalPrimes/Order/KrullDimension.lean, line 732
Order.coheight_pi_eq_iSup_finset	theorem	MinimalPrimes/Order/KrullDimension.lean, line 759
Order.height_pi	theorem	MinimalPrimes/Order/KrullDimension.lean, line 679
Order.coheight_pi	theorem	MinimalPrimes/Order/KrullDimension.lean, line 688
ENat.WithBot.succ_sum_powerset_nonempty	theorem	MinimalPrimes/Data/ENat/BigOperators.lean, line 45
Order.krullDim_toLex_pi	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1551
Order.krullDim_toLex_sigma	theorem	MinimalPrimes/Order/KrullDimension.lean, line 1596
PrimeSpectrum.piHomeomorphUltrafilter	def	MinimalPrimes/RingTheory/Spectrum/Prime/PiUltrafilter.lean, line 183
Ideal.minimalPrimes_span_singleton_eq_normalizedFactors	theorem	MinimalPrimes/Principal.lean, line 138
Ideal.normalizedFactorsEquivMinimalPrimes	def	MinimalPrimes/Principal.lean, line 186
Ideal.normalizedFactorsEquivIrreducibleComponents	def	MinimalPrimes/IrreducibleComponents.lean, line 37
Ideal.associatedPrimes_quotient_span_singleton_eq_minimalPrimes	theorem	MinimalPrimes/AssociatedPrincipal.lean, line 150
IsAssociatedPrime.comap_algebraMap_iff	theorem	MinimalPrimes/AssociatedRestrictScalars.lean, line 68
Ideal.height_span_singleton_le_one_of_prime	theorem	MinimalPrimes/RingTheory/Ideal/PrincipalPrimeHeight.lean, line 48
Ideal.height_span_singleton_eq_one_of_prime_of_mem_nonZeroDivisors	theorem	MinimalPrimes/RingTheory/Ideal/PrincipalPrimeHeight.lean, line 69
Ideal.height_span_singleton_eq_one_of_prime	theorem	MinimalPrimes/RingTheory/Ideal/PrincipalPrimeHeight.lean, line 77
Order.wellFoundedLT_Iic_of_height_lt_top	theorem	MinimalPrimes/Order/FiniteHeightChain.lean, line 36
PrimeSpectrum.exists_stable_of_antitone_of_height_lt_top	theorem	MinimalPrimes/RingTheory/Ideal/FiniteHeightChain.lean, line 53
Ideal.exists_stable_of_antitone_of_finiteHeight	theorem	MinimalPrimes/RingTheory/Ideal/FiniteHeightChain.lean, line 77
RingHom.IsIntegral.ringKrullDim_le	theorem	MinimalPrimes/RingTheory/KrullDimension/Integral.lean, line 43
RingHom.IsIntegral.ringKrullDim_eq	theorem	MinimalPrimes/RingTheory/KrullDimension/Integral.lean, line 54
RingHom.IsIntegral.ringKrullDim_eq_quotient_ker	theorem	MinimalPrimes/RingTheory/KrullDimension/Integral.lean, line 75
Algebra.IsIntegral.ringKrullDim_eq	theorem	MinimalPrimes/RingTheory/KrullDimension/Integral.lean, line 88

Quoted from the main results in formalization.yaml of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.