Documentation Verification Report

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` `commSemiring` `WithBot` `ENat` `WithBot.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `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` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`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` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ringKrullDim` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commSemiring` `WithBot.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instCommSemiringENat` `Distrib.toMul` `WithBot.instCommSemiring` `LinearOrder.toDecidableEq` `instLinearOrderENat` `instCanonicallyOrderedAddENat` `instNoZeroDivisorsENat` `instNontrivialENat` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `WithBot.one` `AddMonoidWithOne.toOne`	—	`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` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instCommSemiringENat` `WithBot.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`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