Theorems · Theorem · field theory

Polynomial.IsUnitTrinomial.irreducible_aux3

∀ {p q : Polynomial ℤ} {k m m' n : ℕ},
  k < m →
    m < n →
      k < m' →
        m' < n →
          ∀ (u v w x z : ℤˣ),
            p = Polynomial.trinomial k m n ↑u ↑v ↑w →
              q = Polynomial.trinomial k m' n ↑x ↑v ↑z → p * p.mirror = q * q.mirror → q = p ∨ q = p.mirror

Defined in: Mathlib.Algebra.Polynomial.UnitTrinomial
Cited by: 1 results in Mathlib
Foundations: Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites43

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Polynomialstatement and proof · cited by 5,681
mul_oneproof · cited by 3,885
Unitsstatement and proof · cited by 2,804
mul_commproof · cited by 2,262
LT.lt.leproof · cited by 2,189
Units.valstatement and proof · cited by 1,966
mul_assocproof · cited by 1,667
add_commproof · cited by 1,535
Polynomial.evalproof · cited by 796
add_assocproof · cited by 746
one_powproof · cited by 521
Polynomial.leadingCoeffproof · cited by 498

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.IsUnitTrinomial.irreducible_of_coprimeproof · cited by 2