Tower

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

Statistics

Metric	Count
Definitions	0
Theorems aeval_algebraMap_apply, aeval_algebraMap_eq_zero_iff, aeval_algebraMap_eq_zero_iff_of_injective, aeval_map_algebraMap, aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C, aeval_coe	6
Total	6

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_algebraMap_apply 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	aeval_def hom_eval₂ IsScalarTower.algebraMap_eq
aeval_algebraMap_eq_zero_iff 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	aeval_algebraMap_apply Algebra.algebraMap_eq_smul_one smul_eq_zero IsDomain.toIsCancelMulZero one_ne_zero' NeZero.one
aeval_algebraMap_eq_zero_iff_of_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	aeval_algebraMap_apply RingHom.map_zero
aeval_map_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval map algebraMap	—	aeval_def eval₂_map IsScalarTower.algebraMap_eq
aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C 📖	mathematical	Multiset Multiset.instMembership DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike mapAlg Multiset.prod CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	aeval_map_algebraMap IsScalarTower.right mapAlg_eq_map map_multiset_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Multiset.prod_eq_zero Multiset.map_map Multiset.mem_map eval_sub eval_X eval_C sub_self

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_coe 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval Subalgebra SetLike.instMembership instSetLike toSemiring algebra	—	Polynomial.aeval_algebraMap_apply isScalarTower_mid IsScalarTower.left IsScalarTower.right

---

← Back to Index