Commit 2026-10-18 08:13 911003dd

feat(RingTheory/Valuation): valuation of an algebraic element (#40197) We prove that if x is algebraic over K then there exists some n ≠ 0 such that the valuation of x raised to the n-th power is equal to the valuation of some element of K.