Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 07:50 e6b84992

View on Github →

feat(ring_theory/valuation/valuation_subring): Adds some equivalent conditions for equivalence of valuations (#13895)

Estimated changes

Modified src/ring_theory/valuation/basic.lean

added theorem valuation.is_equiv_iff_val_eq_one

added theorem valuation.is_equiv_iff_val_le_one

added theorem valuation.map_add_eq_of_lt_left

added theorem valuation.map_add_eq_of_lt_right

Modified src/ring_theory/valuation/valuation_subring.lean

added theorem valuation.is_equiv_iff_valuation_subring

added theorem valuation.is_equiv_valuation_valuation_subring

added theorem valuation.mem_valuation_subring_iff

added def valuation.valuation_subring

added theorem valuation_subring.valuation_subring_valuation