Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-01 07:55 e68503ad

View on Github →

feat(ring_theory/valuation): definition and basic properties of valuations (#3222) From the perfectoid project.

Estimated changes

added theorem eq_one_of_pow_eq_one
added theorem one_le_pow_iff
added theorem one_le_pow_of_one_le'
added theorem pow_eq_one_iff
added theorem pow_le_one_iff
added theorem pow_le_one_of_le_one
added theorem valuation.coe_coe
added def valuation.comap
added theorem valuation.comap_comp
added theorem valuation.comap_id
added theorem valuation.comap_supp
added theorem valuation.ext
added theorem valuation.ext_iff
added theorem valuation.is_equiv.map
added def valuation.map
added theorem valuation.map_add
added theorem valuation.map_add_supp
added theorem valuation.map_inv
added theorem valuation.map_mul
added theorem valuation.map_neg
added theorem valuation.map_neg_one
added theorem valuation.map_one
added theorem valuation.map_pow
added theorem valuation.map_sub_swap
added theorem valuation.map_zero
added theorem valuation.mem_supp_iff
added theorem valuation.ne_zero_iff
added def valuation.supp
added theorem valuation.supp_quot
added theorem valuation.unit_map_eq
added theorem valuation.zero_iff
added structure valuation