Units

📁 Source: Mathlib/Algebra/Polynomial/Degree/Units.lean

Statistics

Metric	Count
Definitions	0
Theorems C_dvd_iff_isUnit, degree_pos_of_not_isUnit, natDegree_pos_of_not_isUnit, coeff_coe_units_zero_ne_zero, degree_coe_units, degree_eq_zero_of_isUnit, degree_pos_of_not_isUnit_of_dvd_monic, isUnit_iff, natDegree_coe_units, natDegree_eq_zero_of_isUnit, natDegree_pos_of_not_isUnit_of_dvd_monic, not_isUnit_of_degree_pos, not_isUnit_of_natDegree_pos	13
Total	13

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_coe_units_zero_ne_zero 📖	—	—	—	—	natDegree_coe_units leadingCoeff.eq_1 leadingCoeff_eq_zero Units.ne_zero nontrivial
degree_coe_units 📖	mathematical	—	degree Units.val Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring WithBot WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	degree_eq_zero_of_isUnit
degree_eq_zero_of_isUnit 📖	mathematical	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	degree WithBot WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	LE.le.antisymm natDegree_eq_zero_iff_degree_le_zero natDegree_eq_zero_of_isUnit zero_le_degree_iff IsUnit.ne_zero nontrivial
degree_pos_of_not_isUnit_of_dvd_monic 📖	mathematical	Monic CommSemiring.toSemiring IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	—	Mathlib.Tactic.Contrapose.contrapose₂ eq_C_of_degree_le_zero Monic.C_dvd_iff_isUnit
isUnit_iff 📖	mathematical	—	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C	—	eq_C_of_natDegree_eq_zero natDegree_eq_zero_of_isUnit isUnit_C
natDegree_coe_units 📖	mathematical	—	natDegree Units.val Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_of_subsingleton natDegree_eq_of_degree_eq_some degree_coe_units
natDegree_eq_zero_of_isUnit 📖	mathematical	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	natDegree	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_of_subsingleton IsUnit.exists_right_inv natDegree_mul left_ne_zero_of_mul_eq_one nontrivial right_ne_zero_of_mul_eq_one add_eq_zero Unique.instSubsingleton natDegree_one
natDegree_pos_of_not_isUnit_of_dvd_monic 📖	mathematical	Monic CommSemiring.toSemiring IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring commSemiring	natDegree	—	natDegree_pos_iff_degree_pos degree_pos_of_not_isUnit_of_dvd_monic
not_isUnit_of_degree_pos 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	subsingleton_or_nontrivial Unique.instSubsingleton degree_eq_zero_of_isUnit
not_isUnit_of_natDegree_pos 📖	mathematical	natDegree	IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	not_isUnit_of_degree_pos natDegree_pos_iff_degree_pos

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_dvd_iff_isUnit 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring	Polynomial semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring Polynomial.commSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	isUnit_iff_dvd_one Polynomial.C_dvd_iff_dvd_coeff coeff_natDegree IsUnit.dvd IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
degree_pos_of_not_isUnit 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass Polynomial.degree	—	degree_pos isUnit_one
natDegree_pos_of_not_isUnit 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring IsUnit Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.natDegree	—	natDegree_pos isUnit_one

---

← Back to Index