Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-28 10:34 e8f8de67

View on Github →

feat(ring_theory/valuation): ring of integers (#4729)

Estimated changes

Modified src/algebra/linear_ordered_comm_group_with_zero.lean

added theorem pow_lt_pow'

added theorem pow_lt_pow_succ

added theorem zero_lt_one''

Modified src/ring_theory/valuation/basic.lean

added theorem valuation.map_add_le

added theorem valuation.map_add_lt

added theorem valuation.map_sum_le

added theorem valuation.map_sum_lt'

added theorem valuation.map_sum_lt

Created src/ring_theory/valuation/integers.lean

added theorem valuation.integer.integers

added def valuation.integer

added theorem valuation.integers.dvd_iff_le

added theorem valuation.integers.dvd_of_le

added theorem valuation.integers.is_unit_of_one

added theorem valuation.integers.le_iff_dvd

added theorem valuation.integers.le_of_dvd

added theorem valuation.integers.one_of_is_unit

added structure valuation.integers

Created src/ring_theory/valuation/integral.lean

added theorem valuation.integers.mem_of_integral