Ideal

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

Statistics

Metric	Count
Definitions	0
Theorems exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top, mem_ideal_map_adjoin, ker_constantCoeff, ker_evalRingHom, ker_modByMonicHom, mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero	6
Total	6

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top 📖	mathematical	Ideal Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet Subalgebra.toSemiring SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Polynomial.instCommSemiringAdjoinSingleton id Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Subalgebra.algebra Ideal.span subset_adjoin Top.top Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	Submodule.setLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Polynomial.leadingCoeff AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra AlgHom.funLike Polynomial.aeval Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	subset_adjoin Ideal.add_eq_one_iff Ideal.add_eq_sup Ideal.one_eq_top mem_ideal_map_adjoin Ideal.mem_span_singleton adjoin_eq_exists_aeval Polynomial.coeff_sub Polynomial.coeff_one_zero Polynomial.mul_coeff_zero Polynomial.coeff_X_zero MulZeroClass.zero_mul sub_zero sub_sub_cancel_left NonUnitalSubringClass.toNegMemClass instNonUnitalSubringClassIdeal Polynomial.reverse_leadingCoeff Polynomial.trailingCoeff_eq_coeff_zero zero_sub Polynomial.eval₂_reverse_eq_zero_iff Polynomial.eval₂_sub Polynomial.eval₂_one add_sub_cancel_left Polynomial.eval₂_mul Polynomial.eval₂_X sub_self
mem_ideal_map_adjoin 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet Ideal Subalgebra.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.map RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap Subalgebra.algebra Polynomial.coeff DFunLike.coe AlgHom Polynomial Polynomial.semiring Polynomial.algebraOfAlgebra id AlgHom.funLike Polynomial.aeval	—	Submodule.span_induction Polynomial.coeff_C AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Polynomial.aeval_C Polynomial.aeval_zero Polynomial.coeff_add AddMemClass.add_mem AddSubmonoidClass.toAddMemClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass adjoin_eq_exists_aeval Polynomial.coeff_mul sum_mem Ideal.mul_mem_left map_mul NonUnitalAlgSemiHomClass.toMulHomClass Polynomial.aeval_mem_adjoin_singleton SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass AddSubmonoidClass.coe_finset_sum Finset.sum_congr DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_X smul_def Ideal.mul_mem_right Ideal.instIsTwoSided Ideal.mem_map_of_mem

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_constantCoeff 📖	mathematical	—	RingHom.ker Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike RingHom.instRingHomClass constantCoeff Ideal.span Set Set.instSingletonSet X	—	le_antisymm RingHom.instRingHomClass Ideal.mem_span_singleton coeff_X_zero
ker_evalRingHom 📖	mathematical	—	RingHom.ker Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike RingHom.instRingHomClass evalRingHom Ideal.span Set Set.instSingletonSet instSub CommRing.toRing X DFunLike.coe C	—	Ideal.ext RingHom.instRingHomClass
ker_modByMonicHom 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring	LinearMap.ker Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing module Semiring.toModule RingHom.id Semiring.toNonAssocSemiring modByMonicHom Submodule.restrictScalars semiring NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toSMul algebraOfAlgebra Algebra.id IsScalarTower.right Ideal.span Set Set.instSingletonSet	—	Submodule.ext IsScalarTower.right mem_ker_modByMonic Ideal.mem_span_singleton
mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span Set Set.instInsert DFunLike.coe RingHom RingHom.instFunLike C instSub CommRing.toRing X Set.instSingletonSet ring eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Ideal.mem_span_pair eval_add eval_mul eval_C eval_sub eval_X sub_self MulZeroClass.mul_zero add_zero dvd_iff_isRoot X_sub_C_dvd_sub_C_eval mul_comm eq_add_of_sub_eq' C_mul

---

← Back to Index