Polynomial

📁 Source: Mathlib/RingTheory/KrullDimension/Polynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems ringKrullDim_of_isNoetherianRing, height_eq_height_add_one, height_map_C, ringKrullDim_le, ringKrullDim_of_isNoetherianRing	5
Total	5

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringKrullDim_of_isNoetherianRing 📖	mathematical	—	ringKrullDim MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid WithBot ENat WithBot.add instAddENat WithBot.natCast ENat.instNatCast Nat.card	—	Finite.induction_empty_option ringKrullDim_eq_of_ringEquiv Nat.card_congr ringKrullDim_mvPolynomial_of_isEmpty PEmpty.instIsEmpty Nat.card_eq_fintype_card Fintype.card_eq_zero CharP.cast_eq_zero CharP.ofCharZero WithBot.charZero add_zero Fintype.card_option Nat.cast_add Nat.cast_one Polynomial.ringKrullDim_of_isNoetherianRing isNoetherianRing Finite.of_fintype

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
height_eq_height_add_one 📖	mathematical	—	Ideal.height Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commRing ENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Ideal.over_def Ideal.IsPrime.under Ideal.IsMaximal.isPrime' Localization.AtPrime.isLocalRing Localization.AtPrime.map_eq_maximalIdeal IsLocalRing.maximalIdeal.isMaximal MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Set.disjoint_left SetLike.mem_coe Ideal.LiesOver.over Ideal.mem_comap algebraMap_eq IsLocalization.comap_map_of_isPrime_disjoint isLocalization Localization.isLocalization Ideal.IsMaximal.isPrime Ideal.IsMaximal.of_isLocalization_of_disjoint IsLocalization.liesOver_of_isPrime_of_disjoint instIsScalarTowerPolynomial OreLocalization.instIsScalarTower IsScalarTower.right isScalarTower IsLocalization.height_map_of_disjoint Disjoint.symm IsLocalization.instIsNoetherianRingLocalization
height_map_C 📖	mathematical	—	Ideal.height Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commRing Ideal.map RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C	—	Ideal.IsMaximal.eq_of_le Ideal.IsPrime.ne_top' Ideal.IsPrime.under Ideal.isPrime_map_C_of_isPrime Ideal.IsMaximal.isPrime' Ideal.le_comap_map Ideal.instIsTwoSided_1 Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown isNoetherianRing Algebra.HasGoingDown.of_flat Module.Flat.of_free instFree Ideal.map_quotient_self Ideal.height_bot IsDomain.toNontrivial Ideal.Quotient.isDomain add_zero
ringKrullDim_le 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat ringKrullDim Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring WithBot.add instAddENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring WithBot.instCommSemiring LinearOrder.toDecidableEq instLinearOrderENat instCommSemiringENat OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat instCanonicallyOrderedAddENat instNoZeroDivisorsENat instNontrivialENat instOfNatAtLeastTwo WithBot.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Nat.instAtLeastTwoHAddOfNat ringKrullDim.eq_1 Order.krullDim_le_of_krullDim_preimage_le' Ideal.comap_mono RingHom.instRingHomClass PrimeSpectrum.isPrime Order.krullDim_eq_of_orderIso ringKrullDim_eq_of_ringEquiv Ring.krullDimLE_iff IsPrincipalIdealRing.krullDimLE_one EuclideanDomain.to_principal_ideal_domain
ringKrullDim_of_isNoetherianRing 📖	mathematical	—	ringKrullDim Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring WithBot ENat WithBot.add instAddENat WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	le_antisymm Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim ringKrullDim_eq_bot_of_subsingleton ringKrullDim_le_iff_isMaximal_height_le height_eq_height_add_one Ideal.over_under WithBot.coe_add WithBot.coe_one add_le_add_left WithBot.addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top' Ideal.IsPrime.under Ideal.IsMaximal.isPrime' ringKrullDim_succ_le_ringKrullDim_polynomial

---

← Back to Index