Ideal

📁 Source: Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean

Statistics

Metric	Count
Definitions	0
Theorems coeff_mem_pow_of_mem_adjoin_C_mul_X, exists_monic_aeval_eq_zero_forall_mem_of_mem_map, exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map	4
Total	4

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_mem_pow_of_mem_adjoin_C_mul_X 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Subalgebra semiring algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin setOf Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instMul DFunLike.coe RingHom RingHom.instFunLike C X	Submodule.instPowNat IsScalarTower.right coeff	—	Algebra.adjoin_induction IsScalarTower.right coeff_C_mul coeff_X mul_one MulZeroClass.mul_zero pow_one AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass coeff_C pow_zero Ideal.one_eq_top coeff_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass coeff_mul sum_mem Ideal.mul_mem_mul pow_add
exists_monic_aeval_eq_zero_forall_mem_of_mem_map 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike algebraMap	Monic DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing coeff	—	IsScalarTower.right exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map Ne.lt_or_gt Ideal.pow_le_self coeff_eq_zero_of_natDegree_lt AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral 📖	mathematical	IsIntegral Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Subalgebra semiring algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin setOf Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instMul DFunLike.coe RingHom RingHom.instFunLike C X Subalgebra.toCommRing commRing ring CommRing.toRing Subalgebra.toAlgebra commSemiring Ring.toSemiring algebra	Monic AlgHom AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.instPowNat IsScalarTower.right natDegree coeff	—	subsingleton_or_nontrivial IsScalarTower.right Monic.leadingCoeff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero Ideal.one_eq_top natDegree_eq_of_le_of_coeff_ne_zero natDegree_sum_le_of_forall_le LE.le.trans natDegree_C_mul_X_pow_le Nat.instNoMaxOrder finset_sum_coeff Finset.sum_congr coeff_C_mul coeff_X_pow mul_ite mul_one MulZeroClass.mul_zero Finset.sum_ite_eq IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass tsub_self coeff_one_zero NeZero.one map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass aeval_C map_pow MonoidWithZeroHomClass.toMonoidHomClass aeval_X mul_pow mul_left_comm RingHom.instRingHomClass coeff_mul_X_pow' mul_comm coeff_map eval₂_eq_sum_range coeff_mem_pow_of_mem_adjoin_C_mul_X AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom RingHom.instFunLike algebraMap	Monic DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.instPowNat IsScalarTower.right natDegree coeff	—	exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral Submodule.span_induction Algebra.subset_adjoin map_mul map_C map_X isIntegral_algebraMap map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass add_mul Distrib.rightDistribClass IsIntegral.add map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass mul_assoc IsIntegral.mul IsIntegral.tower_top IsScalarTower.subalgebra' instIsScalarTowerPolynomial IsScalarTower.left isScalarTower IsScalarTower.right IsIntegral.map AlgHom.algHomClass Algebra.IsIntegral.isIntegral

---

← Back to Index