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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike C	—	aeval_algebraMap_apply AddMonoidAlgebra.isScalarTower IsScalarTower.right
aeval_algebraMap_apply 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap 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	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	aeval_algebraMap_apply RingHom.map_zero
aeval_map_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom MvPolynomial AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike aeval RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval Subalgebra SetLike.instMembership instSetLike toCommSemiring algebra	—	MvPolynomial.aeval_algebraMap_apply IsScalarTower.subalgebra' IsScalarTower.right

---

← Back to Index