Factorization

Statistics

Metric	Count
Definitions	0
Theorems `eq_isMonicOfDegree_one_mul_isMonicOfDegree`, `eq_isMonicOfDegree_one_or_two_mul`, `eq_isMonicOfDegree_two_mul_isMonicOfDegree`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_isMonicOfDegree_one_mul_isMonicOfDegree` 📖	mathematical	`Polynomial.IsMonicOfDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Polynomial` `Polynomial.instMul`	—	`Polynomial.exists_monic_irreducible_factor` `Polynomial.not_isUnit_of_natDegree_pos` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.natDegree_eq_of_degree_eq_some` `IsAlgClosed.degree_eq_one_of_irreducible` `of_mul_left` `add_comm`
`eq_isMonicOfDegree_one_or_two_mul` 📖	mathematical	`Polynomial.IsMonicOfDegree` `Real` `Real.semiring`	`Polynomial` `Polynomial.instMul`	—	`Polynomial.exists_monic_irreducible_factor` `Polynomial.not_isUnit_of_natDegree_pos` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_le_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.IntervalCases.of_lt_left` `Irreducible.natDegree_pos` `Irreducible.natDegree_le_two`
`eq_isMonicOfDegree_two_mul_isMonicOfDegree` 📖	mathematical	`Polynomial.IsMonicOfDegree` `Real` `Real.semiring`	`Polynomial` `Polynomial.instMul`	—	`eq_isMonicOfDegree_one_or_two_mul` `of_mul_left` `add_comm` `mul` `mul_assoc` `mul_left_comm`

---