Commit 2026-04-28 15:17 7148ff9d

feat(Valuation/IsTrivialOn): transcendental_of_lt_one (#37512) For a K-algebra L and a valuation v over L which is trivial on K, if y : L is such that y ≠ 0 and v y < 1, then it is transcendental over K. To add this result we need some lemmas from RatFunc.AsPolynomial which are not related to RatFunc so I have pulled them out of that file. I also didn't want to put this in Valuation.Basic so I have made a new file for valuation which are trivial over some base ring.