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 IsLocalRing.ResidueField.finite_of_module_finite Algebra.IsIntegral.isLocalHom IsPurelyInseparable.isIntegral isPurelyInseparable_self Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsLocalRing.toNontrivial Localization.AtPrime.isLocalRing Module.Finite.self IsLocalRing.ResidueField.instIsScalarTower_1 Localization.AtPrime.instIsScalarTower_1 RingHom.injective DivisionRing.isSimpleRing Field.instIsLocalRing instIsDomain 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 Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker 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 Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker 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 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