UnitTrinomial

Statistics

Metric	Count
Definitions	0
Theorems `irreducible_of_coprime'`	1
Total	1

Name	Kind	Assumes	Proves	Validates	Depends On
`irreducible_of_coprime'` 📖	mathematical	`Polynomial.IsUnitTrinomial` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Int.instCommSemiring` `Complex` `Polynomial.semiring` `Complex.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Ring.toIntAlgebra` `Complex.instRing` `AlgHom.funLike` `Polynomial.aeval` `Complex.instZero` `Polynomial.mirror`	`Irreducible` `Int.instSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`irreducible_of_coprime` `Complex.exists_root` `Polynomial.degree_map_eq_of_injective` `RingHom.injective_int` `Complex.instCharZero` `Polynomial.natDegree_pos_iff_degree_pos` `Polynomial.aeval_mul` `Polynomial.eval_map_algebraMap` `Polynomial.IsRoot.eq_1` `MulZeroClass.zero_mul` `leadingCoeff_isUnit` `isUnit_of_mul_isUnit_left` `instIsDedekindFiniteMonoid` `Polynomial.leadingCoeff_mul` `NormMulClass.toNoZeroDivisors` `Int.instNormMulClass` `Polynomial.eq_C_of_natDegree_eq_zero` `not_lt` `Polynomial.isUnit_C`

---