Pi

📁 Source: Mathlib/RingTheory/Algebraic/Pi.lean

Statistics

Metric	Count
Definitions algebraPi, hasSMulPi, hasSMulPi'	3
Theorems algebraMap_pi_eq_aeval, algebraMap_pi_self_eq_eval, polynomial_smul_apply, polynomial_smul_apply'	4
Total	7

Polynomial

Definitions

Name	Category	Theorems
algebraPi 📖	CompOp	2 math math: algebraMap_pi_eq_aeval, algebraMap_pi_self_eq_eval
hasSMulPi 📖	CompOp	1 math math: polynomial_smul_apply
hasSMulPi' 📖	CompOp	1 math math: polynomial_smul_apply'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_pi_eq_aeval 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring Semiring.toNonAssocSemiring commSemiring Pi.semiring RingHom.instFunLike algebraMap algebraPi AlgHom semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	—
algebraMap_pi_self_eq_eval 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring Semiring.toNonAssocSemiring commSemiring Pi.semiring RingHom.instFunLike algebraMap algebraPi Algebra.id eval	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
polynomial_smul_apply 📖	mathematical	—	Polynomial Polynomial.hasSMulPi Polynomial.eval	—	—
polynomial_smul_apply' 📖	mathematical	—	Polynomial CommSemiring.toSemiring Polynomial.hasSMulPi' DFunLike.coe AlgHom Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	—

---

← Back to Index