Commit 2021-03-02 22:25 19ed0f8e

View on Github →

refactor(ring_theory/valuation): valuations in linear_ordered_comm_monoid_with_zero (#6500) Generalizes the value group in a valuation to a linear_ordered_comm_monoid_with_zero

Estimated changes

Modified src/ring_theory/valuation/basic.lean

modified theorem valuation.is_equiv_of_map_strict_mono

modified theorem valuation.is_equiv_of_val_le_one

modified theorem valuation.ne_zero_iff

modified theorem valuation.zero_iff