Theorem Valuation.exists_map_eq_of_map_sum_eq_zero

Modification history

2026-10-18 08:13

Mathlib/RingTheory/Valuation/Basic.lean

feat(RingTheory/Valuation): valuation of an algebraic element (#40197) …

Added Valuation.exists_map_eq_of_map_sum_eq_zero View on Github →