Polynomial

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

Statistics

Metric	Count
Definitions	0
Theorems map_under_lt_comap_of_quasiFiniteAt, map_under_lt_comap_of_weaklyQuasiFiniteAt, not_ker_le_map_C_of_surjective_of_quasiFiniteAt, not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt, not_quasiFiniteAt, not_weaklyQuasiFiniteAt	6
Total	6

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_under_lt_comap_of_quasiFiniteAt 📖	mathematical	—	Ideal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike C Ideal.under Ideal.comap RingHomClass.toRingHom AlgHom algebraOfAlgebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instRingHomClass	—	map_under_lt_comap_of_weaklyQuasiFiniteAt Algebra.WeaklyQuasiFiniteAt.instOfQuasiFiniteAt
map_under_lt_comap_of_weaklyQuasiFiniteAt 📖	mathematical	—	Ideal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike C Ideal.under Ideal.comap RingHomClass.toRingHom AlgHom algebraOfAlgebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instRingHomClass	—	lt_of_le_of_ne AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instRingHomClass Ideal.map_le_iff_le_comap Ideal.comap_comap algebraMap_eq AlgHom.comp_algebraMap le_refl Ideal.IsPrime.under Ideal.over_under instIsLocalHomAtPrimeRingHomAlgebraMap Algebra.WeaklyQuasiFiniteAt.finite_residueField Ideal.under_liesOver_of_liesOver IsScalarTower.of_algHom Module.Finite.of_injective isNoetherian_of_isNoetherianRing_of_finite instIsNoetherianRingOfIsArtinianRing instIsArtinianOfIsSemisimpleModuleOfFinite IsSemisimpleRing.isSemisimpleModule instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors RingHomInvPair.ids IsLocalRing.ResidueField.instIsScalarTower_1 Localization.AtPrime.instIsScalarTower_1 RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Module.Finite.of_surjective RingHomSurjective.ids AlgEquiv.surjective RatFunc.transcendental_X IsIntegral.isAlgebraic Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral Algebra.IsAlgebraic.of_finite
not_ker_le_map_C_of_surjective_of_quasiFiniteAt 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom semiring algebraOfAlgebra Algebra.id AlgHom.funLike	Ideal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker AlgHom algebraOfAlgebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Ideal.map RingHom RingHom.instFunLike C Ideal.under	—	not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt Algebra.WeaklyQuasiFiniteAt.instOfQuasiFiniteAt
not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom semiring algebraOfAlgebra Algebra.id AlgHom.funLike	Ideal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker AlgHom algebraOfAlgebra Algebra.id AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass Ideal.map RingHom RingHom.instFunLike C Ideal.under	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Ideal.IsPrime.under le_bot_iff RingHom.instRingHomClass Ideal.map_le_iff_le_comap coeff_map Algebra.to_smulCommClass Ideal.instIsTwoSided_1 Ideal.instIsTwoSidedBot PrimeSpectrum.isPrime PrimeSpectrum.ext Ideal.over_def Ideal.over_under Equiv.surjective Algebra.WeaklyQuasiFiniteAt.baseChange not_weaklyQuasiFiniteAt IsScalarTower.right Ideal.IsPrime.comap Algebra.WeaklyQuasiFiniteAt.comap_algEquiv
not_quasiFiniteAt 📖	mathematical	—	Algebra.QuasiFiniteAt Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commRing algebraOfAlgebra Algebra.id	—	not_weaklyQuasiFiniteAt Algebra.WeaklyQuasiFiniteAt.instOfQuasiFiniteAt
not_weaklyQuasiFiniteAt 📖	mathematical	—	Algebra.WeaklyQuasiFiniteAt Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commRing algebraOfAlgebra Algebra.id	—	Module.Finite.of_injective isNoetherian_of_isNoetherianRing_of_finite instIsNoetherianRingOfIsArtinianRing instIsArtinianOfIsSemisimpleModuleOfFinite IsSemisimpleRing.isSemisimpleModule instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.free_of_finite_type_torsion_free' instIsPrincipalIdealRingOfIsSemisimpleRing instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Algebra.WeaklyQuasiFiniteAt.finite_locoalization RingHomInvPair.ids OreLocalization.instIsScalarTower IsScalarTower.right IsLocalization.injective Localization.isLocalization Ideal.primeCompl_le_nonZeroDivisors instNoZeroDivisors IsDomain.to_noZeroDivisors transcendental_X IsIntegral.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing Algebra.IsIntegral.isIntegral Algebra.IsAlgebraic.isIntegral Algebra.IsAlgebraic.of_finite Ideal.IsPrime.under PrimeSpectrum.isPrime Equiv.surjective Algebra.to_smulCommClass Algebra.WeaklyQuasiFiniteAt.baseChange RingHom.instRingHomClass Ideal.IsPrime.comap Algebra.WeaklyQuasiFiniteAt.comap_algEquiv Field.toIsField

---

← Back to Index