Pisot numbers

DefinitionPisot number#✓fully proved

A Pisot number is a real algebraic integer greater than one whose other complex conjugates all have norm less than one.

public def IsPisotNumber (q : ℝ) : Prop :=
  IsIntegral ℤ q ∧ 1 < q ∧
    ∀ β ∈ ((minpoly ℤ q).map (Int.castRingHom ℂ)).roots,
      β ≠ (q : ℂ) → ‖β‖ < 1

Used by 1

Used byUnique Pisot root of a polynomial

DefinitionUnique Pisot root of a polynomial#✓fully proved

Let \(P\) be a polynomial with real coefficients and \(r\) a real number. Then \(r\) is the unique Pisot root of \(P\) when \(r\) is a Pisot number with \(P(r) = 0\) and every Pisot number \(s\) with \(P(s) = 0\) equals \(r\).

public def IsUniquePisotRoot (P : Polynomial ℝ) (r : ℝ) : Prop :=
  IsPisotNumber r ∧ P.IsRoot r ∧
    ∀ s, IsPisotNumber s → P.IsRoot s → s = r

Uses 1

Statement usesPisot number

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.