Irreducible

📁 Source: Mathlib/Algebra/Polynomial/Eval/Irreducible.lean

Statistics

Metric	Count
Definitions	0
Theorems irreducible_of_irreducible_map	1
Total	1

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
irreducible_of_irreducible_map 📖	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Irreducible Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map	—	—	Irreducible.not_isUnit IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.leadingCoeff_mul IsDomain.to_noZeroDivisors Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid mul_comm Irreducible.isUnit_or_isUnit Polynomial.map_mul

---

← Back to Index