Tower

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

Statistics

Metric	Count
Definitions	0
Theorems aeval_C_comp_left, aeval_algebraMap_apply, aeval_algebraMap_eq_zero_iff, aeval_algebraMap_eq_zero_iff_of_injective, aeval_map_algebraMap, mvPolynomial_aeval_coe	6
Total	6

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_C_comp_left 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	aeval_algebraMap_apply isScalarTower IsScalarTower.right
aeval_algebraMap_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	aeval_def coe_eval₂Hom map_eval₂Hom IsScalarTower.algebraMap_eq
aeval_algebraMap_eq_zero_iff 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra 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 MvPolynomial commSemiring algebra Algebra.id AlgHom.funLike aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	aeval_algebraMap_apply RingHom.map_zero
aeval_map_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring commSemiring algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map algebraMap	—	aeval_def eval₂_map IsScalarTower.algebraMap_eq

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mvPolynomial_aeval_coe 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Subalgebra SetLike.instMembership instSetLike toCommSemiring algebra	—	MvPolynomial.aeval_algebraMap_apply IsScalarTower.subalgebra' IsScalarTower.right

---

← Back to Index