Commit 2023-03-18 07:48 21c773a1

View on Github →

feat: Port/RingTheory.Valuation.Integers (#2966) mostly simple fixes: proofs to sub for trans_rel_right and moving instance declarations into namespace.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Valuation/Integers.lean

added theorem Valuation.Integers.dvd_iff_le

added theorem Valuation.Integers.dvd_of_le

added theorem Valuation.Integers.isUnit_of_one

added theorem Valuation.Integers.le_iff_dvd

added theorem Valuation.Integers.le_of_dvd

added theorem Valuation.Integers.one_of_isUnit

added structure Valuation.Integers

added theorem Valuation.integer.integers

added def Valuation.integer