[isabelle] valuation v_2 operator ?

Dear Isabelle users,

I'd like to ask if there already exists a definition/formalization of the valuation v_2 (2-order valuation operator) and its properties in the library ?
i.e. of  v_2 a = Max A where "A = {k∈ ℕ . 2^k dvd a } " ?
(see https://en.wikipedia.org/wiki/Singly_and_doubly_even#Definitions)

Many thanks in advance!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.