Documentation Verification Report

SpecificDegree

📁 Source: Mathlib/Algebra/Polynomial/SpecificDegree.lean

Statistics

Metric	Count
Definitions	0
Theorems `irreducible_iff_roots_eq_zero_of_degree_le_three`, `irreducible_iff_roots_eq_zero_of_degree_le_three`, `irreducible_of_degree_le_three_of_not_isRoot`	3
Total	3

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_iff_roots_eq_zero_of_degree_le_three` 📖	mathematical	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Multiset` `Multiset.instZero`	—	`natDegree_zero` `instIsDomain` `irreducible_mul_leadingCoeff_inv` `Monic.irreducible_iff_roots_eq_zero_of_degree_le_three` `monic_mul_leadingCoeff_inv` `natDegree_mul_leadingCoeff_inv` `mul_comm` `roots_C_mul` `inv_ne_zero` `leadingCoeff_ne_zero`
`irreducible_of_degree_le_three_of_not_isRoot` 📖	mathematical	`Finset` `Finset.instMembership` `Finset.Icc` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsRoot`	`Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	—	`instIsDomain` `irreducible_iff_roots_eq_zero_of_degree_le_three` `Finset.mem_Icc` `Multiset.eq_zero_of_forall_notMem` `irreducible_of_degree_eq_one` `Nat.cast_one` `degree_eq_iff_natDegree_eq_of_pos` `Nat.instZeroLEOneClass` `le_antisymm` `not_le`

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_iff_roots_eq_zero_of_degree_le_three` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.natDegree`	`Irreducible` `Polynomial` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.roots` `Multiset` `Multiset.instZero`	—	`ne_zero` `IsDomain.toNontrivial` `Polynomial.natDegree_one` `irreducible_iff_lt_natDegree_lt` `IsDomain.to_noZeroDivisors` `LE.le.antisymm` `Polynomial.mem_roots` `Polynomial.monic_X_sub_C` `Polynomial.natDegree_X_sub_C` `eq_X_add_C` `sub_neg_eq_add` `Polynomial.C_neg`

---

← Back to Index