The "house" of an algebraic integer

Stream: Is there code for X?

[Michail Karatarakis]

Do we want the "house" of an algebraic integer in mathlib (if it's not there) ?

Let $K$ be an algebraic number field of degree $h,$ and let $\beta_1, \ldots , \beta_h$ be an integer basis, so that every integer in $K$ has the unique representation $a_1\beta_1 + \ldots + a_h\beta_h$ where $a_1, \ldots , a_h$ are rational integers.

If $a$ is an algebraic integer with $a = a_1\beta_1 + \ldots + a_h\beta_h,$ then the ''house'' of $a$ is denoted by $\overline{| a |}$ and is the largest modulus of its conjugates $a^{(i)}$ of $a,$ that is $\overline{| a |} = max_{(1 \leq i \leq h)} | a^{(i)} |.$