Namespace Valuation 3 theorems
- Dominant leading term of a valuation at a pole
Valuation.map_eval_eq_pow_of_one_lt0 below · cited by 1 · depth 9 - Normalised valuation determined by a one-sided inclusion of valuation rings
Valuation.eq_comap_of_valuationSubring_le_comap0 below · cited by 1 · depth 10 - A discrete valuation from factorisation by a parameter t
Valuation.exists_le_one_iff_exists_eq_mk_of_forall_exists_eq_pow_mul0 below · cited by 1 · depth 22