Liouville Inequality in Lean

Stream: mathlib4

[Dcvg5kTele]

After reading some tutos, I thought I was ready to write my own lean scripts. But no luck. I wanted to begin by an easy proposition: Liouville inequality. Let $K/mathbb Q$ be a finite extension of degree $n$; $x\in K$ not zero, and $d\in Z$ such that $dx$ is an algebraic integer. Then, one has
$$|x|\ge\(max(|\sigma(x)|,d))^{-2n}$$
for any morphism $\sigma in Gal(\overline{\Q}/\mathbb Q)$.
Obviously, I want to use mathlib to do that. Not starting from scratch.
It seemed easy, but no luck. If someone could help me, it would be nice. Thanks in advance.

[Kim Morrison]

I suspect you're a bit miscalibrated on "easy" here.

Have you tried writing just the statement (not the proof) in Lean? (Or, as easier steps, do you know how to find the names Mathlib uses for "finite extension", "algebraic integer", and "Galois group"?)

moogle.ai, leansearch.net, and simply grep in the Mathlib source are all great tools for getting started on these problems.