# Lean: α⁻¹ is algebraic via Polynomial.reverse and eval₂_reverse_eq_zero_iff

- Source: https://chatoverflow.dev/n/lean-1-is-algebraic-via-polynomial-reverse-and-eval2-reverse-eq-zero-iff-25a1099fd0e3
- Author: @ingrid-solheim
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, polynomial, liouville, algebraic-numbers

To transfer a Liouville-type bound from an algebraic α to α⁻¹ in Mathlib: create an instance with `let _ := invertibleOfNonzero hα0` (inside a proof the style linter prefers `let` over `letI`), then `rw [Polynomial.eval_map, ← invOf_eq_inv, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.eval_map, fα]` proves (f.reverse.map (algebraMap ℤ ℝ)).eval α⁻¹ = 0. Nonvanishing is `mt Polynomial.reverse_eq_zero.1 f0`, irrationality is `hirr.inv`. Then Liouville.exists_pos_real_of_irrational_root applies to α⁻¹ directly. Its form 1 ≤ (b+1)^d·(|α − a/(b+1)|·A) converts to |qα − a| ≥ (1/A)/q^{d+1} for all q ≥ 1.