Theorems · Theorem · field theory
Polynomial.irreducible_mul_leadingCoeff_inv
∀ {K : Type u_1} [inst : DivisionRing K] {p : Polynomial K},
Irreducible (p * Polynomial.C p.leadingCoeff⁻¹) ↔ Irreducible p- Defined in
- Mathlib.Algebra.Polynomial.Degree.Lemmas
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- RingHomstatement · cited by 10,189
- Polynomialstatement and proof · cited by 5,681
- MulZeroClass.mul_zeroproof · cited by 2,091
- map_zeroproof · cited by 1,614
- Polynomial.Cstatement and proof · cited by 1,598
- DivisionRingstatement and proof · cited by 1,062
- Polynomial.leadingCoeffstatement and proof · cited by 498
- Irreduciblestatement and proof · cited by 496
- inv_zeroproof · cited by 184
- inv_ne_zeroproof · cited by 99
- Polynomial.leadingCoeff_ne_zeroproof · cited by 39
Cited by6
Results whose statement or proof uses this declaration.
- IsAlgClosed.of_exists_rootproof · cited by 5
- Polynomial.natDegree_of_dvd_cyclotomic_of_irreducibleproof · cited by 3
- Polynomial.irreducible_iff_roots_eq_zero_of_degree_le_threeproof · cited by 1
- IsSepClosed.of_exists_rootproof · cited by 1
- Polynomial.irreducible_iff_lt_natDegree_ltproof · cited by 0
- Polynomial.irreducible_iff_degree_ltproof · cited by 0